blob: 5827257b538ea90c279e9870ed433d1d5460d336 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Recommendations in using the API:
The type of terms: constr (see kernel/constr.ml and kernel/term.ml)
- On type constr, the canonical equality on CIC (up to
alpha-conversion and cast removal) is Constr.equal
- The type constr is abstract, use mkRel, mkSort, etc. to build
elements in constr; use "kind_of_term" to analyze the head of a
constr; use destRel, destSort, etc. when the head constructor is
known
|
