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

def Lean.mkNatLookupTable (i type : Expr) (es : Array Expr) : MetaM 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.