Lean.Elab.MutualDef

source

structure Lean.Elab.DefViewElabHeader:

Type

ref : Lean.Syntax
modifiers : Lean.Elab.Modifiers
kind : Lean.Elab.DefKind
shortDeclName : Lean.Name
declName : Lean.Name
levelNames : List Lean.Name
binderIds : Array Lean.Syntax
numParams : Nat
type : Lean.Expr
valueStx : Lean.Syntax

source

instance Lean.Elab.instInhabitedDefViewElabHeader:

Inhabited Lean.Elab.DefViewElabHeader

Equations

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

source

@[inline]

abbrev Lean.Elab.Term.MutualClosure.UsedFVarsMap:

Type

Equations

Lean.Elab.Term.MutualClosure.UsedFVarsMap = Lean.FVarIdMap Lean.FVarIdSet

source

structure Lean.Elab.Term.MutualClosure.FixPoint.State:

Type

usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap
modified : Bool

source

@[inline]

abbrev Lean.Elab.Term.MutualClosure.FixPoint.M (α : Type) :

Type

Equations

Lean.Elab.Term.MutualClosure.FixPoint.M = ReaderT (Array Lean.FVarId) (StateM Lean.Elab.Term.MutualClosure.FixPoint.State)

source

def Lean.Elab.Term.MutualClosure.FixPoint.run (letRecFVarIds : Array Lean.FVarId) (usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap) :

Lean.Elab.Term.MutualClosure.UsedFVarsMap

Equations

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

source

@[inline]

abbrev Lean.Elab.Term.MutualClosure.FreeVarMap:

Type

Equations

Lean.Elab.Term.MutualClosure.FreeVarMap = Lean.FVarIdMap (Array Lean.FVarId)

source

structure Lean.Elab.Term.MutualClosure.ClosureState:

Type

newLocalDecls : Array Lean.LocalDecl
localDecls : Array Lean.LocalDecl
newLetDecls : Array Lean.LocalDecl
exprArgs : Array Lean.Expr

source

structure Lean.Elab.Term.MutualClosure.LetRecClosure:

Type

source

@[inline]

abbrev Lean.Elab.Term.MutualClosure.Replacement:

Type

Equations

Lean.Elab.Term.MutualClosure.Replacement = Lean.FVarIdMap Lean.Expr

source

def Lean.Elab.Term.MutualClosure.insertReplacementForMainFns (r : Lean.Elab.Term.MutualClosure.Replacement) (sectionVars : Array Lean.Expr) (mainHeaders : Array Lean.Elab.DefViewElabHeader) (mainFVars : Array Lean.Expr) :

Lean.Elab.Term.MutualClosure.Replacement

Equations

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

source

def Lean.Elab.Term.MutualClosure.insertReplacementForLetRecs (r : Lean.Elab.Term.MutualClosure.Replacement) (letRecClosures : List Lean.Elab.Term.MutualClosure.LetRecClosure) :

Lean.Elab.Term.MutualClosure.Replacement

Equations

Lean.Elab.Term.MutualClosure.insertReplacementForLetRecs r letRecClosures = List.foldl (fun r c => Std.RBMap.insert r c.toLift.fvarId c.closed) r letRecClosures

source

def Lean.Elab.Term.MutualClosure.Replacement.apply (r : Lean.Elab.Term.MutualClosure.Replacement) (e : Lean.Expr) :

Lean.Expr

Equations

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

source

def Lean.Elab.Term.MutualClosure.pushMain (preDefs : Array Lean.Elab.PreDefinition) (sectionVars : Array Lean.Expr) (mainHeaders : Array Lean.Elab.DefViewElabHeader) (mainVals : Array Lean.Expr) :

Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)

Equations

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

source

def Lean.Elab.Term.MutualClosure.pushLetRecs (preDefs : Array Lean.Elab.PreDefinition) (letRecClosures : List Lean.Elab.Term.MutualClosure.LetRecClosure) (kind : Lean.Elab.DefKind) (modifiers : Lean.Elab.Modifiers) :

Array Lean.Elab.PreDefinition

Equations

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

source

def Lean.Elab.Term.MutualClosure.getKindForLetRecs (mainHeaders : Array Lean.Elab.DefViewElabHeader) :

Lean.Elab.DefKind

Equations

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

source

def Lean.Elab.Term.MutualClosure.getModifiersForLetRecs (mainHeaders : Array Lean.Elab.DefViewElabHeader) :

Lean.Elab.Modifiers

Equations

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

source

def Lean.Elab.Term.MutualClosure.main (sectionVars : Array Lean.Expr) (mainHeaders : Array Lean.Elab.DefViewElabHeader) (mainFVars : Array Lean.Expr) (mainVals : Array Lean.Expr) (letRecsToLift : List Lean.Elab.Term.LetRecToLift) :

Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)

Equations

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

source

structure Lean.Elab.Term.MkInstResult:

Type

instVal : Lean.Expr
instType : Lean.Expr
outParams : Array Lean.Expr

Result for mkInst?

source

def Lean.Elab.Term.processDefDeriving (className : Lean.Name) (declName : Lean.Name) :

Lean.Elab.TermElabM Bool

Equations

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

source

def Lean.Elab.Term.eraseAuxDiscr (e : Lean.Expr) :

Lean.CoreM Lean.Expr

Remove auxiliary match discriminant let-declarations.

Equations

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

source

def Lean.Elab.Term.checkForHiddenUnivLevels (allUserLevelNames : List Lean.Name) (preDefs : Array Lean.Elab.PreDefinition) :

Lean.Elab.TermElabM Unit

Equations

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

source

partial def Lean.Elab.Term.checkForHiddenUnivLevels.visitLevel (allUserLevelNames : List Lean.Name) (sTypes : Lean.CollectLevelParams.State) (preDef : Lean.Elab.PreDefinition) (u : Lean.Level) :

ReaderT Lean.Expr Lean.Elab.TermElabM Unit

source

partial def Lean.Elab.Term.checkForHiddenUnivLevels.visit (allUserLevelNames : List Lean.Name) (sTypes : Lean.CollectLevelParams.State) (preDef : Lean.Elab.PreDefinition) (e : Lean.Expr) :

ReaderT Lean.Expr (Lean.MonadCacheT Lean.ExprStructEq Unit Lean.Elab.TermElabM) Unit

source

def Lean.Elab.Term.elabMutualDef (vars : Array Lean.Expr) (views : Array Lean.Elab.DefView) (hints : Lean.Elab.TerminationHints) :

Lean.Elab.TermElabM Unit

Equations

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

source

def Lean.Elab.Term.elabMutualDef.go (vars : Array Lean.Expr) (views : Array Lean.Elab.DefView) (hints : Lean.Elab.TerminationHints) :

Lean.Elab.TermElabM Unit

Equations

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

source

def Lean.Elab.Term.elabMutualDef.processDeriving (views : Array Lean.Elab.DefView) (headers : Array Lean.Elab.DefViewElabHeader) :

Lean.Elab.TermElabM Unit

Equations

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

source

def Lean.Elab.Command.elabMutualDef (ds : Array Lean.Syntax) (hints : Lean.Elab.TerminationHints) :

Lean.Elab.Command.CommandElabM Unit

Equations

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