Lean.Elab.PreDefinition.Basic

source

structure Lean.Elab.PreDefinition :

Type

ref : Lean.Syntax
kind : Lean.Elab.DefKind
levelParams : List Lean.Name
modifiers : Lean.Elab.Modifiers
declName : Lean.Name
type : Lean.Expr
value : Lean.Expr

source

instance Lean.Elab.instInhabitedPreDefinition :

Inhabited Lean.Elab.PreDefinition

Equations

Lean.Elab.instInhabitedPreDefinition = { default := { ref := default, kind := default, levelParams := default, modifiers := default, declName := default, type := default, value := default } }

source

def Lean.Elab.instantiateMVarsAtPreDecls (preDefs : Array Lean.Elab.PreDefinition) :

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

Equations

Lean.Elab.instantiateMVarsAtPreDecls preDefs = Array.mapM (fun preDef => do let a ← liftM (Lean.Meta.instantiateMVars preDef.type) let a_1 ← liftM (Lean.Meta.instantiateMVars preDef.value) pure { ref := preDef.ref, kind := preDef.kind, levelParams := preDef.levelParams, modifiers := preDef.modifiers, declName := preDef.declName, type := a, value := a_1 }) preDefs

source

def Lean.Elab.levelMVarToParamPreDecls (preDefs : Array Lean.Elab.PreDefinition) :

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

Equations

Lean.Elab.levelMVarToParamPreDecls preDefs = StateRefT'.run' (Lean.Elab.levelMVarToParamPreDeclsAux preDefs) 1

source

def Lean.Elab.fixLevelParams (preDefs : Array Lean.Elab.PreDefinition) (scopeLevelNames : List Lean.Name) (allUserLevelNames : List Lean.Name) :

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

Equations

Lean.Elab.fixLevelParams preDefs scopeLevelNames allUserLevelNames = do let levelParams ← Lean.Elab.getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames let us : List Lean.Level := List.map Lean.mkLevelParam levelParams let fixExpr : Lean.Expr → Lean.Expr := fun e => Lean.Expr.replace (fun c => match c with | Lean.Expr.const declName x x_1 => if Array.any preDefs (fun preDef => preDef.declName == declName) 0 (Array.size preDefs) = true then some (Lean.mkConst declName us) else none | x => none) e pure (Array.map (fun preDef => { ref := preDef.ref, kind := preDef.kind, levelParams := levelParams, modifiers := preDef.modifiers, declName := preDef.declName, type := fixExpr preDef.type, value := fixExpr preDef.value }) preDefs)

source

def Lean.Elab.applyAttributesOf (preDefs : Array Lean.Elab.PreDefinition) (applicationTime : Lean.AttributeApplicationTime) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.applyAttributesOf preDefs applicationTime = do let r ← forIn preDefs PUnit.unit fun preDef r => do Lean.Elab.Term.applyAttributesAt preDef.declName preDef.modifiers.attrs applicationTime pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit

source

def Lean.Elab.abstractNestedProofs (preDef : Lean.Elab.PreDefinition) :

Lean.MetaM Lean.Elab.PreDefinition

Equations

Lean.Elab.abstractNestedProofs preDef = if (Lean.Elab.DefKind.isTheorem preDef.kind || Lean.Elab.DefKind.isExample preDef.kind) = true then pure preDef else do let value ← Lean.Meta.abstractNestedProofs preDef.declName preDef.value pure { ref := preDef.ref, kind := preDef.kind, levelParams := preDef.levelParams, modifiers := preDef.modifiers, declName := preDef.declName, type := preDef.type, value := value }

source

def Lean.Elab.addAsAxiom (preDef : Lean.Elab.PreDefinition) :

Lean.MetaM Unit

Equations

Lean.Elab.addAsAxiom preDef = Lean.withRef preDef.ref (Lean.addDecl (Lean.Declaration.axiomDecl { toConstantVal := { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type }, isUnsafe := preDef.modifiers.isUnsafe }))

source

def Lean.Elab.addAndCompileNonRec (preDef : Lean.Elab.PreDefinition) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.addAndCompileNonRec preDef = Lean.Elab.addNonRecAux preDef true true

source

def Lean.Elab.addNonRec (preDef : Lean.Elab.PreDefinition) (applyAttrAfterCompilation : optParam Bool true) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.addNonRec preDef applyAttrAfterCompilation = Lean.Elab.addNonRecAux preDef false applyAttrAfterCompilation

source

def Lean.Elab.eraseRecAppSyntaxExpr (e : Lean.Expr) :

Lean.CoreM Lean.Expr

Equations

Lean.Elab.eraseRecAppSyntaxExpr e = Lean.Core.transform e (fun e => pure (Lean.TransformStep.visit e)) fun e => pure (Lean.TransformStep.done (if Option.isSome (Lean.getRecAppSyntax? e) = true then Lean.Expr.mdataExpr! e else e))

source

def Lean.Elab.eraseRecAppSyntax (preDef : Lean.Elab.PreDefinition) :

Lean.CoreM Lean.Elab.PreDefinition

Equations

Lean.Elab.eraseRecAppSyntax preDef = do let a ← Lean.Elab.eraseRecAppSyntaxExpr preDef.value pure { ref := preDef.ref, kind := preDef.kind, levelParams := preDef.levelParams, modifiers := preDef.modifiers, declName := preDef.declName, type := preDef.type, value := a }

source

def Lean.Elab.addAndCompileUnsafe (preDefs : Array Lean.Elab.PreDefinition) (safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.unsafe) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.addAndCompileUnsafe preDefs safety = do let preDefs ← Array.mapM (fun d => liftM (Lean.Elab.eraseRecAppSyntax d)) preDefs Lean.withRef (Array.getOp preDefs 0).ref do let a ← List.mapM (fun preDef => pure { toConstantVal := { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type }, value := preDef.value, hints := Lean.ReducibilityHints.opaque, safety := safety }) (Array.toList preDefs) let decl : Lean.Declaration := Lean.Declaration.mutualDefnDecl a Lean.addDecl decl Lean.Elab.withSaveInfoContext do let r ← forIn preDefs PUnit.unit fun preDef r => do let a ← Lean.mkConstWithLevelParams preDef.declName Lean.Elab.Term.addTermInfo preDef.ref a none none Lean.Name.anonymous true pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit Lean.Elab.applyAttributesOf preDefs Lean.AttributeApplicationTime.afterTypeChecking let a ← Lean.Elab.compileDecl decl let _do_jp : PUnit → Lean.Elab.TermElabM Unit := fun y => do Lean.Elab.applyAttributesOf preDefs Lean.AttributeApplicationTime.afterCompilation pure () if a = true then do let y ← pure PUnit.unit _do_jp y else pure ()

source

def Lean.Elab.addAndCompilePartialRec (preDefs : Array Lean.Elab.PreDefinition) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.addAndCompilePartialRec preDefs = if Array.all preDefs Lean.Elab.shouldGenCodeFor 0 (Array.size preDefs) = true then Lean.Elab.addAndCompileUnsafe (Array.map (fun preDef => { ref := preDef.ref, kind := preDef.kind, levelParams := preDef.levelParams, modifiers := { docString? := none, visibility := Lean.Elab.Visibility.regular, isNoncomputable := false, recKind := Lean.Elab.RecKind.default, isUnsafe := false, attrs := #[] }, declName := Lean.Compiler.mkUnsafeRecName preDef.declName, type := preDef.type, value := Lean.Expr.replace (fun e => match e with | Lean.Expr.const declName us x => if Array.any preDefs (fun preDef => preDef.declName == declName) 0 (Array.size preDefs) = true then some (Lean.mkConst (Lean.Compiler.mkUnsafeRecName declName) us) else none | x => none) preDef.value }) preDefs) Lean.DefinitionSafety.partial else pure PUnit.unit