This module provides builder for efficient Nat → … functions based on binary decision trees.

def mkNatLookupTable (i type : Lean.Expr) (es : Array Lean.Expr) : Lean.MetaM Lean.Expr

Builds an expression of type Nat → $type that returns the es[i], using binary search. The array must be non-empty.

Equations

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