Lean4
/-- Discrimination tree key. -/
inductive Key where/-- A metavariable. This key matches with anything. -/
| star/-- A metavariable. This key matches with anything. It stores an identifier. -/
| labelledStar (id : Nat)/-- An opaque variable. This key only matches with `Key.star`. -/
| opaque/-- A constant. It stores the name and the arity. -/
| const (declName : Name) (nargs : Nat)/-- A free variable. It stores the `FVarId` and the arity. -/
| fvar (fvarId : FVarId) (nargs : Nat)/-- A bound variable, from a lambda or forall binder.
It stores the De Bruijn index and the arity. -/
| bvar (deBruijnIndex nargs : Nat)/-- A literal. -/
| lit (v : Literal)/-- A sort. Universe levels are ignored. -/
| sort/-- A lambda function. -/
| lam/-- A dependent arrow. -/
| forall/-- A projection. It stores the structure name, the projection index and the arity. -/
| proj (typeName : Name) (idx nargs : Nat)
deriving Inhabited, BEq
