Documentation

Std.Tactic.Lint.Simp

Linter for simplification lemmas #

This files defines several linters that prevent common mistakes when declaring simp lemmas:

  • The hypotheses of the theorem

  • True if this is a conditional rewrite rule

    isConditional : Bool
  • The thing to replace

    lhs : Lean.Expr
  • The result of replacement

    rhs : Lean.Expr

The data associated to a simp theorem.

Instances For

    Given the list of hypotheses, is this a conditional rewrite rule?

    Equations

    Runs the continuation on all the simp theorems encoded in the given type.

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

    Checks whether two expressions are equal for the simplifier. That is, they are reducibly-definitional equal, and they have the same head symbol.

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

    Constructs a message from all the simp theorems encoded in the given type.

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

    Returns true if this is a @[simp] declaration.

    Equations

    Returns the list of elements in the discrimination tree.

    Equations

    Returns the list of elements in the trie.

    Add message msg to any errors thrown inside k.

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

    Render the list of simp lemmas.

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

    A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.

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

    A linter for simp lemmas whose lhs has a variable as head symbol, and which hence never fire.

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

    A linter for commutativity lemmas that are marked simp.

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