Library MetaCoq.Erasure.EAst
Extracted terms
These are the terms produced by extraction: compared to kernel terms,
all proofs and types are translated to tBox or erased (type annotations
at lambda and let-ins, types of fix/cofixpoints), applications
are in binary form and casts are removed.
Record def (term : Set) := { dname : name; dbody : term; rarg : nat }.
Definition map_def {term : Set} (f : term → term) (d : def term) :=
{| dname := d.(dname); dbody := f d.(dbody); rarg := d.(rarg) |}.
Definition test_def {term : Set} (f : term → bool) (d : def term) :=
f d.(dbody).
Definition mfixpoint (term : Set) := list (def term).
Inductive term : Set :=
| tBox : term
| tRel : nat → term
| tVar : ident → term
| tEvar : nat → list term → term
| tLambda : name → term → term
| tLetIn : name → term → term → term
| tApp : term → term → term
| tConst : kername → term
| tConstruct : inductive → nat → term
| tCase : (inductive × nat) →
term → list (nat × term) → term
| tProj : projection → term → term
| tFix : mfixpoint term → nat → term
| tCoFix : mfixpoint term → nat → term.
Fixpoint mkApps t us :=
match us with
| nil ⇒ t
| a :: args ⇒ mkApps (tApp t a) args
end.
Definition mkApp t u := Eval cbn in mkApps t [u].
Definition isApp t :=
match t with
| tApp _ _ ⇒ true
| _ ⇒ false
end.
Definition isLambda t :=
match t with
| tLambda _ _ ⇒ true
| _ ⇒ false
end.
Entries
Constant and axiom entries
Record parameter_entry := { }.
Record definition_entry := {
definition_entry_body : term;
definition_entry_opaque : bool }.
Inductive constant_entry :=
| ParameterEntry (p : parameter_entry)
| DefinitionEntry (def : definition_entry).
Inductive entries
Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
...
with Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 ... | cpnp : Tpnp.
Inductive recursivity_kind :=
| Finite
| CoFinite
| BiFinite .
Inductive local_entry : Set :=
| LocalDef : term → local_entry
| LocalAssum : term → local_entry.
Record one_inductive_entry : Set := {
mind_entry_typename : ident;
mind_entry_arity : term;
mind_entry_template : bool;
mind_entry_consnames : list ident;
mind_entry_lc : list term }.
Record mutual_inductive_entry := {
mind_entry_record : option (option ident);
mind_entry_finite : recursivity_kind;
mind_entry_params : list (ident × local_entry);
mind_entry_inds : list one_inductive_entry;
mind_entry_private : option bool
}.
Local (de Bruijn) variable binding
Local (de Bruijn) let-binding
Local (de Bruijn) context
Mapping over a declaration and context.
Definition map_decl f (d : context_decl) :=
{| decl_name := d.(decl_name);
decl_body := option_map f d.(decl_body);
|}.
Definition map_context f c :=
List.map (map_decl f) c.
Last declaration first
Definition snoc {A} (Γ : list A) (d : A) := d :: Γ.
Notation " Γ ,, d " := (snoc Γ d) (at level 20, d at next level).
Record one_inductive_body : Set := {
ind_name : ident;
ind_kelim : list sort_family;
ind_ctors : list (ident × term
× nat );
ind_projs : list (ident × term) }.
ind_name : ident;
ind_kelim : list sort_family;
ind_ctors : list (ident × term
× nat );
ind_projs : list (ident × term) }.
See mutual_inductive_body from declarations.ml.
See constant_body from declarations.ml
Record constant_body := {
cst_body : option term }.
Inductive global_decl :=
| ConstantDecl : kername → constant_body → global_decl
| InductiveDecl : kername → mutual_inductive_body → global_decl.
Definition global_declarations := list global_decl.
cst_body : option term }.
Inductive global_decl :=
| ConstantDecl : kername → constant_body → global_decl
| InductiveDecl : kername → mutual_inductive_body → global_decl.
Definition global_declarations := list global_decl.
A context of global declarations +
i.e. a global environment