Documentation

Lean.Meta.DiscrTreeTypes

inductive Lean.Meta.DiscrTree.Key:

Type

const: Lean.Name → Nat → Lean.Meta.DiscrTree.Key
fvar: Lean.FVarId → Nat → Lean.Meta.DiscrTree.Key
lit: Lean.Literal → Lean.Meta.DiscrTree.Key
star: Lean.Meta.DiscrTree.Key
other: Lean.Meta.DiscrTree.Key
arrow: Lean.Meta.DiscrTree.Key
proj: Lean.Name → Nat → Lean.Meta.DiscrTree.Key

instance Lean.Meta.DiscrTree.instInhabitedKey:

Inhabited Lean.Meta.DiscrTree.Key

Equations

Lean.Meta.DiscrTree.instInhabitedKey = { default := Lean.Meta.DiscrTree.Key.const default default }

instance Lean.Meta.DiscrTree.instBEqKey:

BEq Lean.Meta.DiscrTree.Key

Equations

Lean.Meta.DiscrTree.instBEqKey = { beq := [anonymous] }

instance Lean.Meta.DiscrTree.instReprKey:

Repr Lean.Meta.DiscrTree.Key

Equations

Lean.Meta.DiscrTree.instReprKey = { reprPrec := [anonymous] }

def Lean.Meta.DiscrTree.Key.hash:

Lean.Meta.DiscrTree.Key → UInt64

Equations

One or more equations did not get rendered due to their size.

instance Lean.Meta.DiscrTree.instHashableKey:

Hashable Lean.Meta.DiscrTree.Key

Equations

Lean.Meta.DiscrTree.instHashableKey = { hash := Lean.Meta.DiscrTree.Key.hash }

inductive Lean.Meta.DiscrTree.Trie (α : Type) :

Type

node: {α : Type} → Array α → Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α) → Lean.Meta.DiscrTree.Trie α

structure Lean.Meta.DiscrTree (α : Type) :

Type

root : Std.PersistentHashMap Lean.Meta.DiscrTree.Key (Lean.Meta.DiscrTree.Trie α)