Documentation

Lean.Elab.Inductive

def Lean.Elab.Command.checkValidInductiveModifier {m : Type → Type} [inst : Monad m] [inst : Lean.MonadError m] (modifiers : Lean.Elab.Modifiers) :

Equations

Lean.Elab.Command.checkValidInductiveModifier modifiers = let _do_jp := fun y => if Lean.Elab.Modifiers.isPartial modifiers = true then Lean.throwError (Lean.toMessageData "invalid use of 'partial' in inductive declaration") else pure PUnit.unit; if modifiers.isNoncomputable = true then do let y ← Lean.throwError (Lean.toMessageData "invalid use of 'noncomputable' in inductive declaration") _do_jp y else do let y ← pure PUnit.unit _do_jp y

def Lean.Elab.Command.checkValidCtorModifier {m : Type → Type} [inst : Monad m] [inst : Lean.MonadError m] (modifiers : Lean.Elab.Modifiers) :

Equations

Lean.Elab.Command.checkValidCtorModifier modifiers = let _do_jp := fun y => let _do_jp := fun y => let _do_jp := fun y => if (Array.size modifiers.attrs != 0) = true then Lean.throwError (Lean.toMessageData "invalid use of attributes in constructor declaration") else pure PUnit.unit; if modifiers.isUnsafe = true then do let y ← Lean.throwError (Lean.toMessageData "invalid use of 'unsafe' in constructor declaration") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if Lean.Elab.Modifiers.isPartial modifiers = true then do let y ← Lean.throwError (Lean.toMessageData "invalid use of 'partial' in constructor declaration") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if modifiers.isNoncomputable = true then do let y ← Lean.throwError (Lean.toMessageData "invalid use of 'noncomputable' in constructor declaration") _do_jp y else do let y ← pure PUnit.unit _do_jp y

structure Lean.Elab.Command.CtorView :

Type

ref : Lean.Syntax
modifiers : Lean.Elab.Modifiers
inferMod : Bool
declName : Lean.Name
binders : Lean.Syntax
type? : Option Lean.Syntax

instance Lean.Elab.Command.instInhabitedCtorView :

Inhabited Lean.Elab.Command.CtorView

Equations

Lean.Elab.Command.instInhabitedCtorView = { default := { ref := default, modifiers := default, inferMod := default, declName := default, binders := default, type? := default } }

structure Lean.Elab.Command.InductiveView :

Type

ref : Lean.Syntax
modifiers : Lean.Elab.Modifiers
shortDeclName : Lean.Name
declName : Lean.Name
levelNames : List Lean.Name
binders : Lean.Syntax
type? : Option Lean.Syntax
ctors : Array Lean.Elab.Command.CtorView
derivingClasses : Array Lean.Elab.DerivingClassView

instance Lean.Elab.Command.instInhabitedInductiveView :

Inhabited Lean.Elab.Command.InductiveView

Equations

Lean.Elab.Command.instInhabitedInductiveView = { default := { ref := default, modifiers := default, shortDeclName := default, declName := default, levelNames := default, binders := default, type? := default, ctors := default, derivingClasses := default } }

structure Lean.Elab.Command.ElabHeaderResult :

Type

instance Lean.Elab.Command.instInhabitedElabHeaderResult :

Inhabited Lean.Elab.Command.ElabHeaderResult

Equations

Lean.Elab.Command.instInhabitedElabHeaderResult = { default := { view := default, lctx := default, localInsts := default, params := default, type := default } }

def Lean.Elab.Command.tmpIndParam :

Equations

Lean.Elab.Command.tmpIndParam = Lean.mkLevelParam `_tmp_ind_univ_param

def Lean.Elab.Command.shouldInferResultUniverse (u : Lean.Level) :

Lean.Elab.TermElabM Bool

Equations

Lean.Elab.Command.shouldInferResultUniverse u = do let u ← liftM (Lean.Meta.instantiateLevelMVars u) if Lean.Level.hasMVar u = true then match Lean.Level.getLevelOffset u with | Lean.Level.mvar mvarId x => do Lean.Elab.Term.assignLevelMVar mvarId Lean.Elab.Command.tmpIndParam pure true | x => Lean.throwError (Lean.toMessageData "cannot infer resulting universe level of inductive datatype, given level contains metavariables " ++ Lean.toMessageData (Lean.mkSort u) ++ Lean.toMessageData ", provide universe explicitly") else pure false

def Lean.Elab.Command.accLevelAtCtor :

Lean.Level → Lean.Level → Nat → Array Lean.Level → Lean.Elab.TermElabM (Array Lean.Level)

def Lean.Elab.Command.mkResultUniverse (us : Array Lean.Level) (rOffset : Nat) :

Equations

Lean.Elab.Command.mkResultUniverse us rOffset = if (Array.isEmpty us && rOffset == 0) = true then Lean.levelOne else let r := Lean.Level.mkNaryMax (Array.toList us); if (rOffset == 0 && !Lean.Level.isZero r && !Lean.Level.isNeverZero r) = true then Lean.Level.normalize (Lean.mkLevelMax r Lean.levelOne) else Lean.Level.normalize r

constant Lean.Elab.Command.bootstrap.inductiveCheckResultingUniverse :

Lean.Option Bool

def Lean.Elab.Command.checkResultingUniverse (u : Lean.Level) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.Command.checkResultingUniverse u = do let a ← Lean.getOptions if Lean.Option.get a Lean.Elab.Command.bootstrap.inductiveCheckResultingUniverse = true then do let u ← liftM (Lean.Meta.instantiateLevelMVars u) if (!Lean.Level.isZero u && !Lean.Level.isNeverZero u) = true then Lean.throwError (Lean.toMessageData "invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'" ++ Lean.toMessageData (Lean.indentD (Lean.MessageData.ofLevel u)) ++ Lean.toMessageData "") else pure PUnit.unit else pure PUnit.unit

@[inline]

abbrev Lean.Elab.Command.Ctor2InferMod :

Type

Equations

Lean.Elab.Command.Ctor2InferMod = Std.HashMap Lean.Name Bool

def Lean.Elab.Command.elabInductiveViews (views : Array Lean.Elab.Command.InductiveView) :

Lean.Elab.Command.CommandElabM Unit

Equations

Lean.Elab.Command.elabInductiveViews views = let view0 := Array.getOp views 0; let ref := view0.ref; do Lean.Elab.Command.runTermElabM (some view0.declName) fun vars => Lean.withRef ref do Lean.Elab.Command.mkInductiveDecl vars views liftM (Lean.Meta.mkSizeOfInstances view0.declName) liftM (Lean.Meta.IndPredBelow.mkBelow view0.declName) let r ← forIn views PUnit.unit fun view r => do liftM (Lean.Meta.mkInjectiveTheorems view.declName) pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit Lean.Elab.Command.applyDerivingHandlers views