Revision - acfd4ea - Definition of quotient types w.r.t. a equivalence relation - origin: https://github.com/EasyCrypt/easycrypt

visit type:

https://github.com/EasyCrypt/easycrypt

29 November 2022, 16:31:34 UTC

Revision acfd4ea7d779487e774eb6aa8c3deeae783aafd8 authored by Pierre-Yves Strub on 16 April 2020, 14:56:46 UTC, committed by Pierre-Yves Strub on 16 April 2020, 14:56:46 UTC

Definition of quotient types w.r.t. a equivalence relation

1 parent 60a7d34

Files
Changes

Permalinks

Tip revision: acfd4ea7d779487e774eb6aa8c3deeae783aafd8 authored by Pierre-Yves Strub on 16 April 2020, 14:56:46 UTC
Definition of quotient types w.r.t. a equivalence relation

Tip revision: acfd4ea

ecHiTacticals.mli

(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2018 - Inria
 * Copyright (c) - 2012--2018 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-C-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
open EcParsetree
open EcCoreGoal
open EcHiGoal

(* -------------------------------------------------------------------- *)
val process1 : ttenv -> ptactic -> FApi.backward
val process  : ttenv -> ptactic list -> proof -> (handle * handle list) * proof

Showing with 0 additions and 0 deletions (0 / 0 diffs computed)

Computing file changes ...