Notations about LTS

def Cslib.LTS.commandCreate_lts__ : Lean.ParserDescr

A command to create an LTS from a labelled transition α → β → α → Prop, robust to use of variable

Equations

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

def Cslib.LTS.command_Lts_transition_notation__ : Lean.ParserDescr

This command adds transition notations for an LTS. This should not usually be called directly, but from the lts attribute.

As an example lts_transition_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 Cslib.LTS.lts_attr : Lean.ParserDescr

This attribute calls the lts_transition_notation command for the annotated declaration.

Equations

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