inductive SurfaceTLAPlus.Token (α : Type u) : Type u

Syntactic tokens of the TLA⁺ language, including unicode and LaTeX-like variants.

α abstracts away the type of PlusCal tokens.

• module {α : Type u} : Token α
• extends {α : Type u} : Token α
• constant {α : Type u} : Token α
• constants {α : Type u} : Token α
• variable {α : Type u} : Token α
• variables {α : Type u} : Token α
• if {α : Type u} : Token α
• then {α : Type u} : Token α
• else {α : Type u} : Token α
• assume {α : Type u} : Token α
• except {α : Type u} : Token α
• let {α : Type u} : Token α
• in {α : Type u} : Token α
• case {α : Type u} : Token α
• choose {α : Type u} : Token α
• instance {α : Type u} : Token α
• other {α : Type u} : Token α
• with {α : Type u} : Token α
• true {α : Type u} : Token α
• false {α : Type u} : Token α
• paren {α : Type u} (isLeft : Bool) : Token α

  Left and right parenthesis ( ).

• brace {α : Type u} (isLeft : Bool) : Token α

  Left and right curly braces { }.

• bracket {α : Type u} (isLeft : Bool) : Token α

  Left and right square brackets [ ].

• «]_» {α : Type u} : Token α
• «>>_» {α : Type u} : Token α
• eqeq {α : Type u} (isUnicode : Bool) : Token α

  Operator definition operator == ≜.

• comma {α : Type u} : Token α
• underscore {α : Type u} : Token α
• colon {α : Type u} : Token α
• prefix {α : Type u} : PrefixOperator → Token α
• infix {α : Type u} : InfixOperator → Token α
• postfix {α : Type u} : PostfixOperator → Token α
• «\A» {α : Type u} : Token α
• «\E» {α : Type u} : Token α
• «|->» {α : Type u} : Token α
• «->» {α : Type u} : Token α
• bang {α : Type u} : Token α
• at {α : Type u} : Token α
• WF_ {α : Type u} : Token α

  The weak-fairness prefix WF_. Lexed as its own token: WF_e is WF_ then identifier e.

• SF_ {α : Type u} : Token α

  The strong-fairness prefix SF_. Lexed as its own token: SF_e is SF_ then identifier e.

• angle {α : Type u} (isLeft : Bool) : Token α

  << >>.

• moduleStart {α : Type u} (len : ℕ) : Token α

  The delimiter ---- with at least 4 dashes.

• moduleEnd {α : Type u} (len : ℕ) : Token α

  The delimiter ==== with at least 4 equal signs.

• identifier {α : Type u} (name : String) : Token α

  A basic TLA⁺ identifier which is not a reserved word.

• inlineComment {α : Type u} (content : String) : Token α

  An inline comment starting with \*.

• blockComment {α : Type u} (content : String) : Token α

  A multiline comment starting with (* and ending with *).

• number {α : Type u} (repr : String) : Token α
• string {α : Type u} (repr : String) : Token α
• pcal {α : Type u} : List α → Token α

  The tokens of a PlusCal algorithm.

def SurfaceTLAPlus.instReprToken.repr {α✝ : Type u_1} [Repr α✝] : Token α✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.if prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.if")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.then prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.then")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.else prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.else")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.let prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.let")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.in prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.in")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.case prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.case")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.with prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.with")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.true prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.true")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.«]_» prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.«]_»")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.«\A» prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.«\\A»")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.«\E» prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.«\\E»")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.«->» prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.«->»")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.bang prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.bang")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.at prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.at")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.WF_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.WF_")).group prec✝
• SurfaceTLAPlus.instReprToken.repr SurfaceTLAPlus.Token.SF_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SurfaceTLAPlus.Token.SF_")).group prec✝

@[implicit_reducible]

instance SurfaceTLAPlus.instReprToken {α✝ : Type u_1} [Repr α✝] : Repr (Token α✝)

Equations

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

@[implicit_reducible]

instance SurfaceTLAPlus.instInhabitedToken {a✝ : Type u_1} : Inhabited (Token a✝)

Equations

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

def SurfaceTLAPlus.instBEqToken.beq {α✝ : Type u_1} [BEq α✝] : Token α✝ → Token α✝ → Bool

Equations

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

@[implicit_reducible]

instance SurfaceTLAPlus.instBEqToken {α✝ : Type u_1} [BEq α✝] : BEq (Token α✝)

Equations

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

@[reducible, inline]

abbrev SurfaceTLAPlus.Token.lparen {α : Type u_1} : Token α

Equations

• SurfaceTLAPlus.Token.lparen = SurfaceTLAPlus.Token.paren true

@[reducible, inline]

abbrev SurfaceTLAPlus.Token.rparen {α : Type u_1} : Token α

Equations

• SurfaceTLAPlus.Token.rparen = SurfaceTLAPlus.Token.paren false

@[reducible, inline]

abbrev SurfaceTLAPlus.Token.lbrace {α : Type u_1} : Token α

Equations

• SurfaceTLAPlus.Token.lbrace = SurfaceTLAPlus.Token.brace true

@[reducible, inline]

abbrev SurfaceTLAPlus.Token.rbrace {α : Type u_1} : Token α

Equations

• SurfaceTLAPlus.Token.rbrace = SurfaceTLAPlus.Token.brace false

@[reducible, inline]

abbrev SurfaceTLAPlus.Token.lbracket {α : Type u_1} : Token α

Equations

• SurfaceTLAPlus.Token.lbracket = SurfaceTLAPlus.Token.bracket true

@[reducible, inline]

abbrev SurfaceTLAPlus.Token.rbracket {α : Type u_1} : Token α

Equations

• SurfaceTLAPlus.Token.rbracket = SurfaceTLAPlus.Token.bracket false

@[reducible, inline]

abbrev SurfaceTLAPlus.Token.langle {α : Type u_1} : Token α

Equations

• SurfaceTLAPlus.Token.langle = SurfaceTLAPlus.Token.angle true

@[reducible, inline]

abbrev SurfaceTLAPlus.Token.rangle {α : Type u_1} : Token α

Equations

• SurfaceTLAPlus.Token.rangle = SurfaceTLAPlus.Token.angle false

@[implicit_reducible]

instance SurfaceTLAPlus.instToStringToken {α : Type u_1} [ToString α] : ToString (Token α)

Equations

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