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.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] }

instance Lean.Meta.DiscrTree.instInhabitedKey :

Inhabited Lean.Meta.DiscrTree.Key

Equations

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

def Lean.Meta.DiscrTree.Key.hash :

Lean.Meta.DiscrTree.Key → UInt64

Equations

Lean.Meta.DiscrTree.Key.hash x = match x with | Lean.Meta.DiscrTree.Key.const n a => mixHash 5237 (mixHash (hash n) (hash a)) | Lean.Meta.DiscrTree.Key.fvar n a => mixHash 3541 (mixHash (hash n) (hash a)) | Lean.Meta.DiscrTree.Key.lit v => mixHash 1879 (hash v) | Lean.Meta.DiscrTree.Key.star => 7883 | Lean.Meta.DiscrTree.Key.other => 2411 | Lean.Meta.DiscrTree.Key.arrow => 17 | Lean.Meta.DiscrTree.Key.proj s i => mixHash 11 (mixHash (hash s) (hash i))

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 α)