Documentation

Lean.Elab.Tactic.Conv.Lets

Conv tactics to manipulate let expressions #

extract_lets #

source
def Lean.Elab.Tactic.Conv.evalExtractLets :
Tactic
Equations
    Instances For

      lift_lets #

      source
      def Lean.Elab.Tactic.Conv.evalLiftLets :
      Tactic
      Equations
        Instances For

          let_to_have #

          source
          def Lean.Elab.Tactic.Conv.evalLetToHave :
          Tactic
          Equations
            Instances For