@[reducible, inline]

abbrev StrataDDM.SizeBounded (α : Type u_1) [SizeOf α] {β : Sort u_2} [SizeOf β] (e : β) (c : Int) : Type u_1

Array ofelements whose sizes are bounded by a value.

Equations

• StrataDDM.SizeBounded α e c = { a : α // ↑(sizeOf a) ≤ ↑(sizeOf e) + c }

structure StrataDDM.ExprF.HNF {α : Type} (e : ExprF α) : Type

Head-normal form for an expression consists of an operation

• fn : ExprF α
• args : SizeBounded (Array (ArgF α)) e 1

def StrataDDM.ExprF.hnf {α : Type} (e0 : ExprF α) : e0.HNF

Equations

• e0.hnf = StrataDDM.ExprF.hnf.aux✝ e0 e0 #[] ⋯