Documentation

Lean.Elab.PreDefinition.WF.TerminationHint

Support for decreasing_by and termination_by' notations #

source
structure Lean.Elab.WF.TerminationHintValue :
Type
Instances For
    source
    instance Lean.Elab.WF.instInhabitedTerminationHintValue :
    Inhabited Lean.Elab.WF.TerminationHintValue
    source
    inductive Lean.Elab.WF.TerminationHint :
    Type
    Instances For
      source
      instance Lean.Elab.WF.instInhabitedTerminationHint :
      Inhabited Lean.Elab.WF.TerminationHint
      source
      def Lean.Elab.WF.expandTerminationHint (terminationHint? : Option Lean.Syntax) (cliques : Array (Array Lake.Name)) :
      Lean.MacroM Lean.Elab.WF.TerminationHint
      Instances For
        source
        def Lean.Elab.WF.TerminationHint.markAsUsed (t : Lean.Elab.WF.TerminationHint) (clique : Array Lake.Name) :
        Lean.Elab.WF.TerminationHint
        Instances For
          source
          def Lean.Elab.WF.TerminationHint.find? (t : Lean.Elab.WF.TerminationHint) (clique : Array Lake.Name) :
          Option Lean.Elab.WF.TerminationHintValue
          Instances For
            source
            def Lean.Elab.WF.TerminationHint.ensureAllUsed (t : Lean.Elab.WF.TerminationHint) :
            Lean.MacroM Unit
            Instances For

              Support for termination_by notation #

              source
              structure Lean.Elab.WF.TerminationByElement :
              Type
              Instances For
                source
                instance Lean.Elab.WF.instInhabitedTerminationByElement :
                Inhabited Lean.Elab.WF.TerminationByElement
                source
                structure Lean.Elab.WF.TerminationByClique :
                Type
                Instances For
                  source
                  inductive Lean.Elab.WF.TerminationBy :
                  Type
                  Instances For
                    source
                    instance Lean.Elab.WF.instInhabitedTerminationBy :
                    Inhabited Lean.Elab.WF.TerminationBy
                    source
                    inductive Lean.Elab.WF.TerminationWF :
                    Type
                    Instances For
                      source
                      def Lean.Elab.WF.expandTerminationBy (hint? : Option Lean.Syntax) (cliques : Array (Array Lake.Name)) :
                      Lean.MacroM Lean.Elab.WF.TerminationBy
                      Instances For
                        source
                        def Lean.Elab.WF.TerminationBy.markAsUsed (t : Lean.Elab.WF.TerminationBy) (cliqueNames : Array Lake.Name) :
                        Lean.Elab.WF.TerminationBy
                        Instances For
                          source
                          def Lean.Elab.WF.TerminationBy.find? (t : Lean.Elab.WF.TerminationBy) (cliqueNames : Array Lake.Name) :
                          Option Lean.Elab.WF.TerminationWF
                          Instances For
                            source
                            def Lean.Elab.WF.TerminationByClique.allImplicit (c : Lean.Elab.WF.TerminationByClique) :
                            Bool
                            Instances For
                              source
                              def Lean.Elab.WF.TerminationByClique.getExplicitElement? (c : Lean.Elab.WF.TerminationByClique) :
                              Option Lean.Elab.WF.TerminationByElement
                              Instances For
                                source
                                def Lean.Elab.WF.TerminationBy.ensureAllUsed (t : Lean.Elab.WF.TerminationBy) :
                                Lean.MacroM Unit
                                Instances For