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)
• declName? : Option Lean.Name

@[reducible, inline]

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

Equations

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

def Auto.Reif.setDeclName? (field : Option Lean.Name) : ReifM PUnit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.getDeclName? : ReifM (Option Lean.Name)

Equations

• Auto.Reif.getDeclName? = do let st ← get pure st.declName?

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.getInds : ReifM (Array (Array SimpleIndVal))

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[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

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