Documentation

Lean.Elab.Inductive

← Mathematical handbook
source
def Lean.Elab.Command.mkInductiveElabDescr (isCoinductive : Bool := false) :
InductiveElabDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Command.elabInductiveCommand :
    InductiveElabDescr
    Equations
    Instances For
      source
      def Lean.Elab.Command.elabCoinductiveCommand :
      InductiveElabDescr
      Equations
      Instances For