https://github.com/EasyCrypt/easycrypt
Tip revision: 452ec9f1509d5aabbaf4924798443fb9df53ede5 authored by François Dupressoir on 14 December 2021, 12:22:51 UTC
Lemma stating equality of word and list distributions
Lemma stating equality of word and list distributions
Tip revision: 452ec9f
ecInductive.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2021 - Inria
* Copyright (c) - 2012--2021 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcSymbols
open EcPath
open EcTypes
open EcCoreFol
open EcDecl
(* -------------------------------------------------------------------- *)
type field = symbol * EcTypes.ty
type fields = field list
type record = {
rc_path : path;
rc_tparams : ty_params;
rc_fields : fields;
}
(* -------------------------------------------------------------------- *)
type ctor = symbol * (EcTypes.ty list)
type ctors = ctor list
type datatype = {
dt_path : path;
dt_tparams : ty_params;
dt_ctors : ctors
}
(* -------------------------------------------------------------------- *)
val record_ctor_name : symbol -> symbol
val record_ind_path : symbol -> symbol
val record_ctor_path : path -> path
val record_ind_path : path -> path
(* -------------------------------------------------------------------- *)
val indsc_of_record : record -> form
(* -------------------------------------------------------------------- *)
val datatype_ind_name : [`Elim|`Case] -> symbol -> symbol
val datatype_ind_path : [`Elim|`Case] -> path -> path
val datatype_proj_name : symbol -> symbol
val datatype_proj_path : path -> symbol -> path
(* -------------------------------------------------------------------- *)
exception NonPositive
val indsc_of_datatype : ?normty:(ty -> ty) -> [`Elim|`Case] -> datatype -> form
val datatype_as_ty_dtype : datatype -> ty_params * ty_dtype
(* -------------------------------------------------------------------- *)
val datatype_projectors :
path * ty_params * ty_dtype -> (symbol * operator) list
(* -------------------------------------------------------------------- *)
type case1 = {
cs1_ctor : EcPath.path;
cs1_vars : (EcIdent.t * EcTypes.ty) list;
}
type branch1 = {
br1_target : EcIdent.t;
br1_case : case1;
}
type branch = {
br_branches : branch1 list;
br_body : expr;
}
type opfix = branch list
(* -------------------------------------------------------------------- *)
val collate_matchfix : EcDecl.opfix -> opfix
(* -------------------------------------------------------------------- *)
type prind = {
ip_path : path;
ip_tparams : ty_params;
ip_prind : EcDecl.prind;
}
val indsc_of_prind : prind -> ty_params * form
val introsc_of_prind : prind -> (symbol * (ty_params * form)) list
val prind_schemes : prind -> (symbol * (ty_params * form)) list
val prind_indsc_name : symbol -> symbol
val prind_indsc_path : path -> path
val prind_introsc_path : path -> symbol -> path
val prind_is_iso_ands : EcDecl.prind -> (symbol * int) option
val prind_is_iso_ors : EcDecl.prind -> (symbol * int) pair option