Documentation

Lean.Elab.Tactic.Conv.Lets

Conv tactics to manipulate let expressions #

extract_lets #

source
def Lean.Elab.Tactic.Conv.evalExtractLets :
Tactic
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    lift_lets #

    source
    def Lean.Elab.Tactic.Conv.evalLiftLets :
    Tactic
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      let_to_have #

      source
      def Lean.Elab.Tactic.Conv.evalLetToHave :
      Tactic
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For