type object_flavour =
[ `Definition
+ | `MutualDefinition
| `Fact
| `Lemma
| `Remark
the record fields names and if they are coercions and
then the coercion arity *)
| `Projection (** record projection *)
+ | `InversionPrinciple (** inversion principle *)
]
type attribute =
| Cast of term * term (* value, type *)
| Prod of name * term * term (* binder, source, target *)
| Lambda of name * term * term (* binder, source, target *)
- | LetIn of name * term * term (* binder, term, target *)
+ | LetIn of name * term * term * term (* binder, term, type, target *)
| Appl of term list (* arguments *)
| Const of UriManager.uri * (* uri, *)
term explicit_named_substitution (* explicit named subst. *)
| ACast of id * annterm * annterm (* value, type *)
| AProd of id * name * annterm * annterm (* binder, source, target *)
| ALambda of id * name * annterm * annterm (* binder, source, target *)
- | ALetIn of id * name * annterm * annterm (* binder, term, target *)
+ | ALetIn of id * name * annterm * annterm * annterm (* binder, term, type, target *)
| AAppl of id * annterm list (* arguments *)
| AConst of id * UriManager.uri * (* uri, *)
annterm explicit_named_substitution (* explicit named subst. *)
and context_entry = (* A declaration or definition *)
Decl of term
- | Def of term * term option (* body, type (if known) *)
+ | Def of term * term (* body, type *)
and hypothesis =
(name * context_entry) option (* None means no more accessible *)
and anncontext_entry = (* A declaration or definition *)
ADecl of annterm
- | ADef of annterm
+ | ADef of annterm * annterm
and annhypothesis =
id * (name * anncontext_entry) option (* None means no more accessible *)