Relations: Attributes

This module defines the reduction_sys attribute used for creating relation notations.

def Relation.command_Reduction_notation__ : Lean.ParserDescr

This command adds notations for relations. This should not usually be called directly, but from the reduction_sys attribute.

As an example reduction_notation foo "β" will add the notations "⭢β" and "↠β".

Note that the string used will afterwards be registered as a notation. This means that if you have also used this as a constructor name, you will need quotes to access corresponding cases, e.g. «β» in the above example.

Equations

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

def Relation.reductionSys : Lean.ParserDescr

This attribute calls the reduction_notation command for the annotated declaration, such as in:

@[reduction_sys "ₙ", simp]
def PredReduction (a b : ℕ) : Prop := a = b + 1

Equations

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