https://github.com/EasyCrypt/easycrypt
Revision 60d29c1f11f6c79824022608f9f83503d983ce61 authored by Benjamin Gregoire on 13 September 2019, 06:39:19 UTC, committed by Benjamin Gregoire on 13 September 2019, 06:39:19 UTC
1 parent 0e717db
Tip revision: 60d29c1f11f6c79824022608f9f83503d983ce61 authored by Benjamin Gregoire on 13 September 2019, 06:39:19 UTC
remove duplicate lemma get_none -> domNE
remove duplicate lemma get_none -> domNE
Tip revision: 60d29c1
ecTheory.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 EcPath
open EcSymbols
open EcDecl
open EcModules
(* -------------------------------------------------------------------- *)
type theory = theory_item list
and theory_item =
| Th_type of (symbol * tydecl)
| Th_operator of (symbol * operator)
| Th_axiom of (symbol * axiom)
| Th_modtype of (symbol * module_sig)
| Th_module of module_expr
| Th_theory of (symbol * (theory * thmode))
| Th_export of EcPath.path
| Th_instance of (ty_params * EcTypes.ty) * tcinstance
| Th_typeclass of (symbol * typeclass)
| Th_baserw of symbol
| Th_addrw of EcPath.path * EcPath.path list
| Th_auto of (bool * int * symbol option * path list)
and tcinstance = [ `Ring of ring | `Field of field | `General of EcPath.path ]
and thmode = [ `Abstract | `Concrete ]
(* -------------------------------------------------------------------- *)
type ctheory = {
cth_desc : ctheory_desc;
cth_struct : ctheory_struct;
}
and ctheory_desc =
| CTh_struct of ctheory_struct
| CTh_clone of ctheory_clone
and ctheory_struct = ctheory_item list
and ctheory_item =
| CTh_type of (symbol * tydecl)
| CTh_operator of (symbol * operator)
| CTh_axiom of (symbol * axiom)
| CTh_modtype of (symbol * module_sig)
| CTh_module of module_expr
| CTh_theory of (symbol * (ctheory * thmode))
| CTh_export of EcPath.path
| CTh_instance of (ty_params * EcTypes.ty) * tcinstance
| CTh_typeclass of (symbol * typeclass)
| CTh_baserw of symbol
| CTh_addrw of EcPath.path * EcPath.path list
| CTh_auto of (bool * int * symbol option * path list)
and ctheory_clone = {
cthc_base : EcPath.path;
cthc_ext : (EcIdent.t * ctheory_override) list;
}
and ctheory_override =
| CTHO_Type of EcTypes.ty
(* -------------------------------------------------------------------- *)
val module_comps_of_module_sig_comps:
module_sig_body -> module_item list
val module_expr_of_module_sig:
EcIdent.t -> module_type -> module_sig -> mod_restr -> module_expr
Computing file changes ...