structure Auto.Reif.State : Type

• facts : Array UMonoFact
• exprFVarVal : Std.HashMap Lean.FVarId Lean.Expr
• tyCanMap : Std.HashMap Lean.Expr Lean.Expr
• inhTys : Array UMonoFact
• inds : Array (Array SimpleIndVal)

@[reducible, inline]

abbrev Auto.Reif.ReifM (α : Type) : Type

Equations

• Auto.Reif.ReifM = StateT Auto.Reif.State Lean.MetaM

def Auto.Reif.setTyCanMap (field : Std.HashMap Lean.Expr Lean.Expr) : ReifM PUnit

Equations

• Auto.Reif.setTyCanMap field = modify fun (st : Auto.Reif.State) => { facts := st.facts, exprFVarVal := st.exprFVarVal, tyCanMap := field, inhTys := st.inhTys, inds := st.inds }

def Auto.Reif.setInds (field : Array (Array SimpleIndVal)) : ReifM PUnit

Equations

• Auto.Reif.setInds field = modify fun (st : Auto.Reif.State) => { facts := st.facts, exprFVarVal := st.exprFVarVal, tyCanMap := st.tyCanMap, inhTys := st.inhTys, inds := field }

def Auto.Reif.getExprFVarVal : ReifM (Std.HashMap Lean.FVarId Lean.Expr)

Equations

• Auto.Reif.getExprFVarVal = do let st ← get pure st.exprFVarVal

def Auto.Reif.getInds : ReifM (Array (Array SimpleIndVal))

Equations

• Auto.Reif.getInds = do let st ← get pure st.inds

def Auto.Reif.getTyCanMap : ReifM (Std.HashMap Lean.Expr Lean.Expr)

Equations

• Auto.Reif.getTyCanMap = do let st ← get pure st.tyCanMap

def Auto.Reif.getInhTys : ReifM (Array UMonoFact)

Equations

• Auto.Reif.getInhTys = do let st ← get pure st.inhTys

def Auto.Reif.setInhTys (field : Array UMonoFact) : ReifM PUnit

Equations

• Auto.Reif.setInhTys field = modify fun (st : Auto.Reif.State) => { facts := st.facts, exprFVarVal := st.exprFVarVal, tyCanMap := st.tyCanMap, inhTys := field, inds := st.inds }

def Auto.Reif.getFacts : ReifM (Array UMonoFact)

Equations

• Auto.Reif.getFacts = do let st ← get pure st.facts

def Auto.Reif.setExprFVarVal (field : Std.HashMap Lean.FVarId Lean.Expr) : ReifM PUnit

Equations

• Auto.Reif.setExprFVarVal field = modify fun (st : Auto.Reif.State) => { facts := st.facts, exprFVarVal := field, tyCanMap := st.tyCanMap, inhTys := st.inhTys, inds := st.inds }

def Auto.Reif.setFacts (field : Array UMonoFact) : ReifM PUnit

Equations

• Auto.Reif.setFacts field = modify fun (st : Auto.Reif.State) => { facts := field, exprFVarVal := st.exprFVarVal, tyCanMap := st.tyCanMap, inhTys := st.inhTys, inds := st.inds }

@[inline]

def Auto.Reif.resolveVal (e : Lean.Expr) : ReifM Lean.Expr

Given an expression e, if it's a fvar and is in polyVal, return its value recorded in exprFVarVal. Otherwise return e

Equations

• Auto.Reif.resolveVal (Lean.Expr.fvar id) = do let __do_lift ← Auto.Reif.getExprFVarVal pure ((__do_lift.get? id).getD (Lean.Expr.fvar id))
• Auto.Reif.resolveVal e = pure e

@[inline]

def Auto.Reif.resolveTy (e : Lean.Expr) : ReifM Lean.Expr

Equations

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

def Auto.Reif.mkAuxName (suffix : Lean.Name) : ReifM Lean.Name

Equations

• Auto.Reif.mkAuxName suffix = Lean.mkAuxDeclName suffix