structure Auto.ExprDeCompile.Context : Type

• usedNames : Std.HashSet String

structure Auto.ExprDeCompile.State : Type

• binderNames : Array String
• curIdx : Nat

@[reducible, inline]

abbrev Auto.ExprDeCompile.ExprDeCompM (α : Type) : Type

Equations

• Auto.ExprDeCompile.ExprDeCompM = ReaderT Auto.ExprDeCompile.Context (StateRefT' IO.RealWorld Auto.ExprDeCompile.State Lean.MetaM)

def Auto.ExprDeCompile.withNewBinder {α : Type} (m : ExprDeCompM α) : ExprDeCompM (α × String)

Equations

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

def Auto.ExprDeCompile.levelCollectNames (l : Lean.Level) : StateT (Std.HashSet String) Lean.MetaM Unit

Equations

• Auto.ExprDeCompile.levelCollectNames Lean.Level.zero = pure PUnit.unit
• Auto.ExprDeCompile.levelCollectNames l_2.succ = Auto.ExprDeCompile.levelCollectNames l_2
• Auto.ExprDeCompile.levelCollectNames (Lean.Level.mvar a) = pure PUnit.unit
• Auto.ExprDeCompile.levelCollectNames (Lean.Level.param n) = modify fun (s : Std.HashSet String) => s.insert n.toString
• Auto.ExprDeCompile.levelCollectNames (l1.max l2) = do Auto.ExprDeCompile.levelCollectNames l1 Auto.ExprDeCompile.levelCollectNames l2
• Auto.ExprDeCompile.levelCollectNames (l1.imax l2) = do Auto.ExprDeCompile.levelCollectNames l1 Auto.ExprDeCompile.levelCollectNames l2

def Auto.ExprDeCompile.exprCollectNames (e : Lean.Expr) : StateT (Std.HashSet String) Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.forallE binderName d b binderInfo) = do Auto.ExprDeCompile.exprCollectNames d Auto.ExprDeCompile.exprCollectNames b
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.lam binderName d b binderInfo) = do Auto.ExprDeCompile.exprCollectNames d Auto.ExprDeCompile.exprCollectNames b
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.mdata data b) = Auto.ExprDeCompile.exprCollectNames b
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.letE declName t v b nonDep) = do Auto.ExprDeCompile.exprCollectNames t Auto.ExprDeCompile.exprCollectNames v Auto.ExprDeCompile.exprCollectNames b
• Auto.ExprDeCompile.exprCollectNames (fn.app arg) = do Auto.ExprDeCompile.exprCollectNames fn Auto.ExprDeCompile.exprCollectNames arg
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.proj typeName idx b) = do Auto.ExprDeCompile.exprCollectNames b modify fun (s : Std.HashSet String) => s.insert typeName.toString
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.lit l) = pure PUnit.unit
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.sort l) = Auto.ExprDeCompile.levelCollectNames l
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.mvar mvarId) = pure PUnit.unit
• Auto.ExprDeCompile.exprCollectNames (Lean.Expr.bvar n) = pure PUnit.unit

def Auto.exprDeCompile (e : Lean.Expr) : Lean.MetaM String

Equations

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