Documentation

Lean.Elab.Inductive

source
def Lean.Elab.Command.mkInductiveElabDescr (isCoinductive : Bool := false) :
InductiveElabDescr
Equations
    Instances For
      source
      def Lean.Elab.Command.elabInductiveCommand :
      InductiveElabDescr
      Equations
        Instances For
          source
          def Lean.Elab.Command.elabCoinductiveCommand :
          InductiveElabDescr
          Equations
            Instances For