structure Lean.Elab.Command.CoinductiveElabData : Type

This structure contains the data carried in InductiveElabStep1 that are solely used in mutual coinductive predicate elaboration.

• declId : Syntax

  Declaration Id from the original InductiveView

• declName : Name

  Declaration name of the predicate

• ref : Syntax

  Ref from the original InductiveView

• modifiers : Modifiers

  Modifiers from the original InductiveView

• ctorSyntax : Array Syntax

  Constructor refs from the original InductiveView

• isGreatest : Bool

  The flag that is true if the predicate was defined via coinductive keyword and false otherwise. When we elaborate a mutual definition, we allow mixing coinductive and inductive keywords, and hence we need to record this information.

instance Lean.Elab.Command.instInhabitedCoinductiveElabData : Inhabited CoinductiveElabData

Equations

• Lean.Elab.Command.instInhabitedCoinductiveElabData = { default := Lean.Elab.Command.instInhabitedCoinductiveElabData.default }

def Lean.Elab.Command.instInhabitedCoinductiveElabData.default : CoinductiveElabData

Equations

• Lean.Elab.Command.instInhabitedCoinductiveElabData.default = { declId := default, declName := default, ref := default, modifiers := default, ctorSyntax := default, isGreatest := default }

def Lean.Elab.Command.addFunctorPostfix : Name → Name

Equations

• Lean.Elab.Command.addFunctorPostfix x✝ = x✝ ++ `_functor

def Lean.Elab.Command.removeFunctorPostfix : Name → Name

Equations

• Lean.Elab.Command.removeFunctorPostfix x✝ = x✝.modifyBase Lean.Name.getPrefix

def Lean.Elab.Command.removeFunctorPostfixInCtor : Name → Name

Equations

• Lean.Elab.Command.removeFunctorPostfixInCtor (p.str s) = (Lean.Elab.Command.removeFunctorPostfix p).str s
• Lean.Elab.Command.removeFunctorPostfixInCtor x✝ = panicWithPosWithDecl "Lean.Elab.Coinductive" "Lean.Elab.Command.removeFunctorPostfixInCtor" 124 13 "UnexpectedName"

def Lean.Elab.Command.elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : TermElabM Unit

Main entry point for elaborating mutual coinductive predicates. This function is called after generating a flat inductive and adding it to the environment.

We look at corresponding existential form of the flat inductive (see Meta.MkIffOfInductiveProp), use it to populate PreDefinitions that correspond to the predicates, and then we call the PartialFixpoint machinery to register them as (co)inductive predicates.

Finally, we generate constructors for each of the predicates, that correspond to the constructors that were given by the user.

Equations

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