Documentation

Lean.Elab.Do.InferControlInfo

source
structure Lean.Elab.Do.ControlInfo :
Type

Represents information about what control effects a do block has.

  • breaks : Bool

    The do block may break.

  • continues : Bool

    The do block may continue.

  • returnsEarly : Bool

    The do block may return early.

  • numRegularExits : Nat

    The number of regular exit paths the do block has. Corresponds to the number of jumps to an ambient join point.

  • reassigns : NameSet

    The variables that are reassigned in the do block.

Instances For
    source
    def Lean.Elab.Do.instInhabitedControlInfo.default :
    ControlInfo
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Elab.Do.instInhabitedControlInfo :
      Inhabited ControlInfo
      source
      def Lean.Elab.Do.ControlInfo.pure :
      ControlInfo
      Instances For
        source
        def Lean.Elab.Do.ControlInfo.sequence (a b : ControlInfo) :
        ControlInfo
        Instances For
          source
          def Lean.Elab.Do.ControlInfo.alternative (a b : ControlInfo) :
          ControlInfo
          Instances For
            source
            @[implicit_reducible]
            instance Lean.Elab.Do.instToMessageDataControlInfo :
            ToMessageData ControlInfo
            source
            @[reducible, inline]
            abbrev Lean.Elab.Do.ControlInfoHandler :
            Type

            A handler for inferring ControlInfo from a doElem syntax. Register with @[doElem_control_info parserName].

            Instances For
              source
              unsafe def Lean.Elab.Do.mkControlInfoElemAttributeUnsafe (ref : Name) :
              IO (KeyedDeclsAttribute ControlInfoHandler)
              Instances For
                source
                @[implemented_by Lean.Elab.Do.mkControlInfoElemAttributeUnsafe]
                opaque Lean.Elab.Do.mkControlInfoElemAttribute (ref : Name) :
                IO (KeyedDeclsAttribute ControlInfoHandler)
                source
                opaque Lean.Elab.Do.controlInfoElemAttribute :
                KeyedDeclsAttribute ControlInfoHandler

                Registers a ControlInfo inference handler for the given doElem syntax node kind.

                A handler should have type ControlInfoHandler (i.e. TSyntax \doElem → TermElabM ControlInfo). For pure handlers, use fun stx => return ControlInfo.pure`.

                source
                partial def Lean.Elab.Do.InferControlInfo.ofElem (stx : TSyntax `doElem) :
                TermElabM ControlInfo
                source
                partial def Lean.Elab.Do.InferControlInfo.ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [`Lean.Parser.Term.doIdDecl, `Lean.Parser.Term.doPatDecl]) :
                TermElabM ControlInfo
                source
                partial def Lean.Elab.Do.InferControlInfo.ofLetOrReassign (reassigned : Array Ident) (rhs? : Option (TSyntax `doElem)) (otherwise? body? : Option (TSyntax `Lean.Parser.Term.doSeqIndent)) :
                TermElabM ControlInfo
                source
                partial def Lean.Elab.Do.InferControlInfo.ofSeq (stx : TSyntax `Lean.Parser.Term.doSeq) :
                TermElabM ControlInfo
                source
                partial def Lean.Elab.Do.InferControlInfo.ofOptionSeq (stx? : Option (TSyntax `Lean.Parser.Term.doSeq)) :
                TermElabM ControlInfo
                source
                def Lean.Elab.Do.inferControlInfoSeq (doSeq : TSyntax `Lean.Parser.Term.doSeq) :
                TermElabM ControlInfo
                Instances For
                  source
                  def Lean.Elab.Do.inferControlInfoElem (doElem : TSyntax `doElem) :
                  TermElabM ControlInfo
                  Instances For