Documentation

Lean.Meta.Tactic.Assert

Convert the given goal Ctx |- target into Ctx |- type -> target. It assumes val has type type

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Add the hypothesis h : t, given v : t, and return the new FVarId.

    Equations
    • g.note h v t? = do let __do_liftmatch t? with | some t => pure t | none => Lean.Meta.inferType v let __do_liftg.assert h __do_lift v __do_lift.intro1P
    Instances For

      Convert the given goal Ctx |- target into Ctx |- let name : type := val; target. It assumes val has type type

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Convert the given goal Ctx |- target into Ctx |- (hName : type) -> hName = val -> target. It assumes val has type type

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Convert the given goal Ctx |- target into a goal containing (userName : type) after the local declaration with if fvarId. It assumes val has type type, and that type is well-formed after fvarId. Note that val does not need to be well-formed after fvarId. That is, it may contain variables that are defined after fvarId.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Instances For

              Convert the given goal Ctx |- target into Ctx, (hs[0].userName : hs[0].type) ... |-target. It assumes hs[i].val has type hs[i].type.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Replace hypothesis hyp in goal g with proof : typeNew. The new hypothesis is given the same user name as the original, it attempts to avoid reordering hypotheses, and the original is cleared if possible.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Finds the LocalDecl for the FVar in e with the highest index.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For