- Naming policy:
- natural numbers : sorts h k, local references i j, lengths l o
- boolean values : p q
- - generic leaf items : m n
- generic binding items: r s
- generic flat items : r s
- generic head items : m n
include "preamble.ma".
-inductive Leaf: Set \def
- | sort: Nat \to Leaf
- | lref: Nat \to Leaf
-.
-
inductive Bind: Set \def
| abbr: Bind
| abst: Bind
.
inductive Term: Set \def
- | leaf: Leaf \to Term
+ | sort: Nat \to Term
+ | lref: Nat \to Term
| intb: IntB \to Term \to Term \to Term
| intf: IntF \to Term \to Term \to Term
.