Eval — computable reduce surface

#eval / #guard wrappers on the already-computable cd and cd_loop_fuel. Imports only Kernel + InvariantLayer (no holonomic weight).

Helpers make it easy to build ISKSubtype values without manual proofs.

ISKSubtype smart constructors

def ISAR.isk_norm : ISKSubtype

Equations

• ISAR.isk_norm = ⟨ISAR.ITerm.norm, ISAR.ISKTerm.norm⟩

def ISAR.isk_konst : ISKSubtype

Equations

• ISAR.isk_konst = ⟨ISAR.ITerm.konst, ISAR.ISKTerm.konst⟩

def ISAR.isk_s : ISKSubtype

Equations

• ISAR.isk_s = ⟨ISAR.ITerm.sₛ, ISAR.ISKTerm.sₛ⟩

def ISAR.isk_app (f x : ISKSubtype) : ISKSubtype

Equations

• f ⬝ x = ⟨f.val · x.val, ⋯⟩

def ISAR.«term_⬝_» : Lean.TrailingParserDescr

Equations

• ISAR.«term_⬝_» = Lean.ParserDescr.trailingNode `ISAR.«term_⬝_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ ") (Lean.ParserDescr.cat `term 71))

@[implicit_reducible]

instance ISAR.instReprISKSubtype : Repr ISKSubtype

Equations

• ISAR.instReprISKSubtype = { reprPrec := fun (t : ISAR.ISKSubtype) (p : Nat) => reprPrec t.val p }

One-shot cd

def ISAR.cd_isk (t : ISKSubtype) : ISKSubtype

Equations

• ISAR.cd_isk t = ⟨ISAR.cd t.val, ⋯⟩

Fuelled reduce (cd strategy)

def ISAR.reduce_cd (fuel : Nat) (t : ISKSubtype) : ISKSubtype

Equations

• ISAR.reduce_cd fuel t = ISAR.cd_loop_fuel fuel t

Golden terms

def ISAR.gold_Ix : ISKSubtype

I x → x

Equations

• ISAR.gold_Ix = ISAR.isk_norm ⬝ ISAR.isk_konst

def ISAR.gold_Kxy : ISKSubtype

K x y → x

Equations

• ISAR.gold_Kxy = ISAR.isk_konst ⬝ ISAR.isk_s ⬝ ISAR.isk_norm

def ISAR.gold_SKKx : ISKSubtype

S K K x → x (SKK is identity)

Equations

• ISAR.gold_SKKx = ISAR.isk_s ⬝ ISAR.isk_konst ⬝ ISAR.isk_konst ⬝ ISAR.isk_norm

def ISAR.gold_B : ISKSubtype

S (K S) K — the B combinator (composition)

Equations

• ISAR.gold_B = ISAR.isk_s ⬝ (ISAR.isk_konst ⬝ ISAR.isk_s) ⬝ ISAR.isk_konst

def ISAR.gold_Bfgx : ISKSubtype

B f g x = f (g x)

Equations

• ISAR.gold_Bfgx = ISAR.gold_B ⬝ ISAR.isk_konst ⬝ ISAR.isk_norm ⬝ ISAR.isk_s

#eval demonstrations

#guard (compile-time checked)