inductive SurfacePlusCal.Token : Type

• fair : Token
• algorithm : Token
• variable : Token
• variables : Token
• define : Token
• process : Token
• if : Token
• else : Token
• while : Token
• with : Token
• skip : Token
• either : Token
• await : Token
• when : Token
• assert : Token
• print : Token
• goto : Token
• or : Token
• semicolon : Token
• barbar : Token
• dashdash : Token
• fifo : Token
• fifos : Token
• channel : Token
• channels : Token
• receive : Token
• multicast : Token
• send : Token
• tla (tk : SurfaceTLAPlus.Token Token) : Token

  Embeds a TLA⁺ token, for parsing TLA⁺ expressions inside PlusCal.

partial def SurfacePlusCal.instReprToken.repr : Token → ℕ → Std.Format

@[implicit_reducible]

instance SurfacePlusCal.instReprToken : Repr Token

Equations

• SurfacePlusCal.instReprToken = { reprPrec := SurfacePlusCal.instReprToken.repr }

@[implicit_reducible]

instance SurfacePlusCal.instInhabitedToken : Inhabited Token

Equations

• SurfacePlusCal.instInhabitedToken = { default := SurfacePlusCal.instInhabitedToken.default }

partial def SurfacePlusCal.instBEqToken.beq : Token → Token → Bool

@[implicit_reducible]

instance SurfacePlusCal.instBEqToken : BEq Token

Equations

• SurfacePlusCal.instBEqToken = { beq := SurfacePlusCal.instBEqToken.beq }

partial def SurfacePlusCal.Token.toString : Token → String

@[implicit_reducible]

instance SurfacePlusCal.instToStringToken : ToString Token

Equations

• SurfacePlusCal.instToStringToken = { toString := SurfacePlusCal.Token.toString }