Documentation

def SurfaceTLAPlus.instBEqPrefixOperator.beq :

PrefixOperator → PrefixOperator → Bool

Equations

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instBEqPrefixOperator :

BEq PrefixOperator

Equations

SurfaceTLAPlus.instBEqPrefixOperator = { beq := SurfaceTLAPlus.instBEqPrefixOperator.beq }

def SurfaceTLAPlus.instReprPrefixOperator.repr :

PrefixOperator → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instReprPrefixOperator :

Repr PrefixOperator

Equations

SurfaceTLAPlus.instReprPrefixOperator = { reprPrec := SurfaceTLAPlus.instReprPrefixOperator.repr }

def SurfaceTLAPlus.instDecidableEqPrefixOperator.decEq (x✝ x✝¹ : PrefixOperator) :

Decidable (x✝ = x✝¹)

Equations

Instances For

DecidableEq PrefixOperator

@[implicit_reducible]

instance SurfaceTLAPlus.instDecidableEqPrefixOperator :

Equations

SurfaceTLAPlus.instDecidableEqPrefixOperator = SurfaceTLAPlus.instDecidableEqPrefixOperator.decEq

@[implicit_reducible]

instance SurfaceTLAPlus.instInhabitedPrefixOperator :

Inhabited PrefixOperator

Equations

SurfaceTLAPlus.instInhabitedPrefixOperator = { default := SurfaceTLAPlus.instInhabitedPrefixOperator.default }

@[reducible, inline]

abbrev SurfaceTLAPlus.PrefixOperator.«\neg» :

PrefixOperator

Equations

SurfaceTLAPlus.PrefixOperator.«\neg» = SurfaceTLAPlus.PrefixOperator.«\neg » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.PrefixOperator.«\lnot» :

PrefixOperator

Equations

SurfaceTLAPlus.PrefixOperator.«\lnot» = SurfaceTLAPlus.PrefixOperator.«\neg » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.PrefixOperator.«~» :

PrefixOperator

Equations

SurfaceTLAPlus.PrefixOperator.«~» = SurfaceTLAPlus.PrefixOperator.«\neg » 2

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instToStringPrefixOperator :

ToString PrefixOperator

Equations

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

inductive SurfaceTLAPlus.PostfixOperator :

The entire set of postfix operators reserved in TLA⁺.

«^+» : PostfixOperator
^+
«^*» : PostfixOperator
^*
«^#» : PostfixOperator
^#
«'» : PostfixOperator
'

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instBEqPostfixOperator :

BEq PostfixOperator

Equations

SurfaceTLAPlus.instBEqPostfixOperator = { beq := SurfaceTLAPlus.instBEqPostfixOperator.beq }

def SurfaceTLAPlus.instBEqPostfixOperator.beq :

PostfixOperator → PostfixOperator → Bool

Equations

SurfaceTLAPlus.instBEqPostfixOperator.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instReprPostfixOperator :

Repr PostfixOperator

Equations

SurfaceTLAPlus.instReprPostfixOperator = { reprPrec := SurfaceTLAPlus.instReprPostfixOperator.repr }

def SurfaceTLAPlus.instReprPostfixOperator.repr :

PostfixOperator → ℕ → Std.Format

Equations

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

Instances For

DecidableEq PostfixOperator

@[implicit_reducible]

instance SurfaceTLAPlus.instDecidableEqPostfixOperator :

Equations

SurfaceTLAPlus.instDecidableEqPostfixOperator x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Inhabited PostfixOperator

@[implicit_reducible]

instance SurfaceTLAPlus.instInhabitedPostfixOperator :

Equations

SurfaceTLAPlus.instInhabitedPostfixOperator = { default := SurfaceTLAPlus.instInhabitedPostfixOperator.default }

@[implicit_reducible]

instance SurfaceTLAPlus.instToStringPostfixOperator :

ToString PostfixOperator

Equations

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

inductive SurfaceTLAPlus.InfixOperator :

The entire set of infix operators reserved in TLA⁺.

«!!» : InfixOperator
## : InfixOperator
«$$» : InfixOperator
«$» : InfixOperator
«%%» : InfixOperator
«%» : InfixOperator
«&&» : InfixOperator
«&» : InfixOperator
«(+) » : Fin 2 → InfixOperator
⊕: (+) or \oplus
«(-) » : Fin 2 → InfixOperator
⊝: (-) or \ominus
«(.) » : Fin 2 → InfixOperator
⊙: (.) or \odot
«(/) » : Fin 2 → InfixOperator
⊘: (/) or \oslash
«(\X) » : Fin 2 → InfixOperator
⊗: (\X) or \otimes
«\X » : Fin 2 → InfixOperator
×: \X or \times. Not actually a binary operator in the grammar, but treated as such for simplicity.
«**» : InfixOperator
«*» : InfixOperator
«++» : InfixOperator
«+» : InfixOperator
«-+->» : InfixOperator
«--» : InfixOperator
«-|» : InfixOperator
⊣: -|
«-» : InfixOperator
«...» : InfixOperator
«..» : InfixOperator
«.» : InfixOperator
«//» : InfixOperator
«/= » : Fin 2 → InfixOperator
≠: /= or #
«/\ » : Fin 2 → InfixOperator
∧: /\ or \land
«/» : InfixOperator
«::=» : InfixOperator
⩴: ::=
«:=» : InfixOperator
≔: :=
«:>» : InfixOperator
«<:» : InfixOperator
«<=> » : Fin 2 → InfixOperator
≡: <=> or \equiv
«=< » : Fin 3 → InfixOperator
≤: =<, <=, or \leq
«=>» : InfixOperator
⇒: =>
«=|» : InfixOperator
⫤: =|
«<» : InfixOperator
«=» : InfixOperator
«>= » : Fin 2 → InfixOperator
≥: >= or \geq
«>» : InfixOperator
?? : InfixOperator
? : InfixOperator
«@@» : InfixOperator
«\/ » : Fin 2 → InfixOperator
∨: \/ or \lor
«^^» : InfixOperator
«^» : InfixOperator
«|-» : InfixOperator
⊢: |-
«|=» : InfixOperator
⊨: |=
«||» : InfixOperator
‖: ||
«|» : InfixOperator
«~>» : InfixOperator
⤳: ~>
«\approx» : InfixOperator
«\sqsupseteq» : InfixOperator
«\asymp» : InfixOperator
«\gg» : InfixOperator
«\star» : InfixOperator
«\bigcirc» : InfixOperator
«\in» : InfixOperator
∈: \in
«\preceq» : InfixOperator
«\prec» : InfixOperator
«\subseteq» : InfixOperator
«\subset» : InfixOperator
«\bullet» : InfixOperator
«\cap » : Fin 2 → InfixOperator
∩: \cap or \intersect
«\propto» : InfixOperator
«\succeq» : InfixOperator
«\succ» : InfixOperator
«\cdot» : InfixOperator
«\simeq» : InfixOperator
«\sim» : InfixOperator
«\ll» : InfixOperator
«\supseteq» : InfixOperator
«\supset» : InfixOperator
«\cong» : InfixOperator
«\sqcap» : InfixOperator
«\cup » : Fin 2 → InfixOperator
∪: \cup or \union
«\o » : Fin 2 → InfixOperator
∘: \o or \circ
«\sqcup» : InfixOperator
«\div» : InfixOperator
«\sqsubseteq» : InfixOperator
«\sqsubset» : InfixOperator
«\uplus» : InfixOperator
«\doteq» : InfixOperator
«\wr» : InfixOperator
«\sqsupset» : InfixOperator
«\notin» : InfixOperator
∉: \notin
«\» : InfixOperator
backslash, \

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instBEqInfixOperator :

BEq InfixOperator

Equations

SurfaceTLAPlus.instBEqInfixOperator = { beq := SurfaceTLAPlus.instBEqInfixOperator.beq }

def SurfaceTLAPlus.instBEqInfixOperator.beq :

InfixOperator → InfixOperator → Bool

Equations

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

Instances For

def SurfaceTLAPlus.instReprInfixOperator.repr :

InfixOperator → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instReprInfixOperator :

Repr InfixOperator

Equations

SurfaceTLAPlus.instReprInfixOperator = { reprPrec := SurfaceTLAPlus.instReprInfixOperator.repr }

@[implicit_reducible]

instance SurfaceTLAPlus.instInhabitedInfixOperator :

Inhabited InfixOperator

Equations

SurfaceTLAPlus.instInhabitedInfixOperator = { default := SurfaceTLAPlus.instInhabitedInfixOperator.default }

def SurfaceTLAPlus.instDecidableEqInfixOperator.decEq (x✝ x✝¹ : InfixOperator) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

DecidableEq InfixOperator

@[implicit_reducible]

instance SurfaceTLAPlus.instDecidableEqInfixOperator :

Equations

SurfaceTLAPlus.instDecidableEqInfixOperator = SurfaceTLAPlus.instDecidableEqInfixOperator.decEq

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«(+)» :

Equations

SurfaceTLAPlus.InfixOperator.«(+)» = SurfaceTLAPlus.InfixOperator.«(+) » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\oplus» :

Equations

SurfaceTLAPlus.InfixOperator.«\oplus» = SurfaceTLAPlus.InfixOperator.«(+) » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«(-)» :

Equations

SurfaceTLAPlus.InfixOperator.«(-)» = SurfaceTLAPlus.InfixOperator.«(-) » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\ominus» :

Equations

SurfaceTLAPlus.InfixOperator.«\ominus» = SurfaceTLAPlus.InfixOperator.«(-) » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«(.)» :

Equations

SurfaceTLAPlus.InfixOperator.«(.)» = SurfaceTLAPlus.InfixOperator.«(.) » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\odot» :

Equations

SurfaceTLAPlus.InfixOperator.«\odot» = SurfaceTLAPlus.InfixOperator.«(.) » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«(/)» :

Equations

SurfaceTLAPlus.InfixOperator.«(/)» = SurfaceTLAPlus.InfixOperator.«(/) » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\oslash» :

Equations

SurfaceTLAPlus.InfixOperator.«\oslash» = SurfaceTLAPlus.InfixOperator.«(/) » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«(\X)» :

Equations

SurfaceTLAPlus.InfixOperator.«(\X)» = SurfaceTLAPlus.InfixOperator.«(\X) » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\otimes» :

Equations

SurfaceTLAPlus.InfixOperator.«\otimes» = SurfaceTLAPlus.InfixOperator.«(\X) » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\X» :

Equations

SurfaceTLAPlus.InfixOperator.«\X» = SurfaceTLAPlus.InfixOperator.«\X » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\times» :

Equations

SurfaceTLAPlus.InfixOperator.«\times» = SurfaceTLAPlus.InfixOperator.«\X » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«/=» :

Equations

SurfaceTLAPlus.InfixOperator.«/=» = SurfaceTLAPlus.InfixOperator.«/= » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«#» :

Equations

SurfaceTLAPlus.InfixOperator.«#» = SurfaceTLAPlus.InfixOperator.«/= » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«/\» :

Equations

SurfaceTLAPlus.InfixOperator.«/\» = SurfaceTLAPlus.InfixOperator.«/\ » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\land» :

Equations

SurfaceTLAPlus.InfixOperator.«\land» = SurfaceTLAPlus.InfixOperator.«/\ » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«<=>» :

Equations

SurfaceTLAPlus.InfixOperator.«<=>» = SurfaceTLAPlus.InfixOperator.«<=> » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\equiv» :

Equations

SurfaceTLAPlus.InfixOperator.«\equiv» = SurfaceTLAPlus.InfixOperator.«<=> » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«=<» :

Equations

SurfaceTLAPlus.InfixOperator.«=<» = SurfaceTLAPlus.InfixOperator.«=< » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«<=» :

Equations

SurfaceTLAPlus.InfixOperator.«<=» = SurfaceTLAPlus.InfixOperator.«=< » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\leq» :

Equations

SurfaceTLAPlus.InfixOperator.«\leq» = SurfaceTLAPlus.InfixOperator.«=< » 2

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«>=» :

Equations

SurfaceTLAPlus.InfixOperator.«>=» = SurfaceTLAPlus.InfixOperator.«>= » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\geq» :

Equations

SurfaceTLAPlus.InfixOperator.«\geq» = SurfaceTLAPlus.InfixOperator.«>= » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\/» :

Equations

SurfaceTLAPlus.InfixOperator.«\/» = SurfaceTLAPlus.InfixOperator.«\/ » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\lor» :

Equations

SurfaceTLAPlus.InfixOperator.«\lor» = SurfaceTLAPlus.InfixOperator.«\/ » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\cap» :

Equations

SurfaceTLAPlus.InfixOperator.«\cap» = SurfaceTLAPlus.InfixOperator.«\cap » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\intersect» :

Equations

SurfaceTLAPlus.InfixOperator.«\intersect» = SurfaceTLAPlus.InfixOperator.«\cap » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\cup» :

Equations

SurfaceTLAPlus.InfixOperator.«\cup» = SurfaceTLAPlus.InfixOperator.«\cup » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\union» :

Equations

SurfaceTLAPlus.InfixOperator.«\union» = SurfaceTLAPlus.InfixOperator.«\cup » 1

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\o» :

Equations

SurfaceTLAPlus.InfixOperator.«\o» = SurfaceTLAPlus.InfixOperator.«\o » 0

Instances For

@[reducible, inline]

abbrev SurfaceTLAPlus.InfixOperator.«\circ» :

Equations

SurfaceTLAPlus.InfixOperator.«\circ» = SurfaceTLAPlus.InfixOperator.«\o » 1

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instToStringInfixOperator :

ToString InfixOperator

Equations

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

inductive SurfaceTLAPlus.Typ :

TLA⁺ types, in the same format as Apalache.

bool : Typ
int : Typ
str : Typ
function : Typ → Typ → Typ
τ -> τ
set : Typ → Typ
Set(τ)
seq : Typ → Typ
Seq(τ)
bag : Typ → Typ
Bag(τ)
tuple : List Typ → Typ
<<τ₁, …, τₙ>>
operator : List Typ → Typ → Typ
(τ₁, …, τₙ) => τₙ₊₁
var : String → Typ
A rigid, universally-quantified type variable a.
const : String → Typ
CONSTANT — an abstract type.
record : List (String × Typ) → Typ
channel : Typ → Typ
Channel(τ). Covariant: τ <: τ' → Channel(τ) <: Channel(τ').
address : Typ
Address.
mvar : ℕ → Typ
A metavariable ?n, resolved during type checking; never appears in a fully-elaborated TypedTLAPlus term.

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instReprTyp :

Repr Typ

Equations

SurfaceTLAPlus.instReprTyp = { reprPrec := SurfaceTLAPlus.instReprTyp.repr }

partial def SurfaceTLAPlus.instReprTyp.repr :

Typ → ℕ → Std.Format

@[implicit_reducible]

instance SurfaceTLAPlus.instInhabitedTyp :

Inhabited Typ

Equations

SurfaceTLAPlus.instInhabitedTyp = { default := SurfaceTLAPlus.instInhabitedTyp.default }

@[implicit_reducible]

instance SurfaceTLAPlus.instBEqTyp :

BEq Typ

Equations

SurfaceTLAPlus.instBEqTyp = { beq := SurfaceTLAPlus.instBEqTyp.beq }

partial def SurfaceTLAPlus.instBEqTyp.beq :

Typ → Typ → Bool

def SurfaceTLAPlus.Typ.isChannelLike :

Typ → Bool

Whether τ is Channel-shaped: a bare Channel(τ'), or an indexed channel family dom -> Channel(τ') (as Elaborator/PlusCal.lean's checkChannelDecl encodes it). Shared by WellFormedness/Declarations.lean (checks 2(a)/(d)) and WellFormedness/Restrictions.lean (check

as one source of truth for "legal channel type."

Equations

x_1.channel.isChannelLike = true
(x_1.function x_2.channel).isChannelLike = true
x✝.isChannelLike = false

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instDecidableEqTyp :

DecidableEq Typ

Equations

SurfaceTLAPlus.instDecidableEqTyp = SurfaceTLAPlus.instDecidableEqTyp.go

partial def SurfaceTLAPlus.instDecidableEqTyp.go (τ τ' : Typ) :

Decidable (τ = τ')

@[implicit_reducible]

instance SurfaceTLAPlus.instToStringTyp :

ToString Typ

Equations

SurfaceTLAPlus.instToStringTyp = { toString := SurfaceTLAPlus.instToStringTyp.go }

partial def SurfaceTLAPlus.instToStringTyp.go :

Typ → String

inductive SurfaceTLAPlus.QuantifierBound (α β : Type) :

Groups of variables bound in quantifiers (\A/\E/…).

var {α β : Type} : α → String → β → QuantifierBound α β
x ∈ A
varTuple {α β : Type} : List (α × String) → β → QuantifierBound α β
⟨x, y, …, z⟩ ∈ A
vars {α β : Type} : List (α × String) → β → QuantifierBound α β
x, y, …, z ∈ A

Instances For

def SurfaceTLAPlus.instReprQuantifierBound.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] :

QuantifierBound α✝ β✝ → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instReprQuantifierBound {α✝ β✝ : Type} [Repr α✝] [Repr β✝] :

Repr (QuantifierBound α✝ β✝)

Equations

SurfaceTLAPlus.instReprQuantifierBound = { reprPrec := SurfaceTLAPlus.instReprQuantifierBound.repr }

def SurfaceTLAPlus.instDecidableEqQuantifierBound.decEq {α✝ β✝ : Type} [DecidableEq α✝] [DecidableEq β✝] (x✝ x✝¹ : QuantifierBound α✝ β✝) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
SurfaceTLAPlus.instDecidableEqQuantifierBound.decEq (SurfaceTLAPlus.QuantifierBound.var a a_1 a_2) (SurfaceTLAPlus.QuantifierBound.varTuple a_3 a_4) = isFalse ⋯
SurfaceTLAPlus.instDecidableEqQuantifierBound.decEq (SurfaceTLAPlus.QuantifierBound.var a a_1 a_2) (SurfaceTLAPlus.QuantifierBound.vars a_3 a_4) = isFalse ⋯
SurfaceTLAPlus.instDecidableEqQuantifierBound.decEq (SurfaceTLAPlus.QuantifierBound.varTuple a a_1) (SurfaceTLAPlus.QuantifierBound.var a_2 a_3 a_4) = isFalse ⋯
SurfaceTLAPlus.instDecidableEqQuantifierBound.decEq (SurfaceTLAPlus.QuantifierBound.varTuple a a_1) (SurfaceTLAPlus.QuantifierBound.vars a_2 a_3) = isFalse ⋯
SurfaceTLAPlus.instDecidableEqQuantifierBound.decEq (SurfaceTLAPlus.QuantifierBound.vars a a_1) (SurfaceTLAPlus.QuantifierBound.var a_2 a_3 a_4) = isFalse ⋯
SurfaceTLAPlus.instDecidableEqQuantifierBound.decEq (SurfaceTLAPlus.QuantifierBound.vars a a_1) (SurfaceTLAPlus.QuantifierBound.varTuple a_2 a_3) = isFalse ⋯

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instDecidableEqQuantifierBound {α✝ β✝ : Type} [DecidableEq α✝] [DecidableEq β✝] :

DecidableEq (QuantifierBound α✝ β✝)

Equations

SurfaceTLAPlus.instDecidableEqQuantifierBound = SurfaceTLAPlus.instDecidableEqQuantifierBound.decEq

def SurfaceTLAPlus.instBEqQuantifierBound.beq {α✝ β✝ : Type} [BEq α✝] [BEq β✝] :

QuantifierBound α✝ β✝ → QuantifierBound α✝ β✝ → Bool

Equations

SurfaceTLAPlus.instBEqQuantifierBound.beq (SurfaceTLAPlus.QuantifierBound.var a a_1 a_2) (SurfaceTLAPlus.QuantifierBound.var b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
SurfaceTLAPlus.instBEqQuantifierBound.beq (SurfaceTLAPlus.QuantifierBound.varTuple a a_1) (SurfaceTLAPlus.QuantifierBound.varTuple b b_1) = (a == b && a_1 == b_1)
SurfaceTLAPlus.instBEqQuantifierBound.beq (SurfaceTLAPlus.QuantifierBound.vars a a_1) (SurfaceTLAPlus.QuantifierBound.vars b b_1) = (a == b && a_1 == b_1)
SurfaceTLAPlus.instBEqQuantifierBound.beq x✝¹ x✝ = false

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instBEqQuantifierBound {α✝ β✝ : Type} [BEq α✝] [BEq β✝] :

BEq (QuantifierBound α✝ β✝)

Equations

SurfaceTLAPlus.instBEqQuantifierBound = { beq := SurfaceTLAPlus.instBEqQuantifierBound.beq }

def SurfaceTLAPlus.QuantifierBound.bimap {α β γ δ : Type} (f : α → γ) (g : β → δ) :

QuantifierBound α β → QuantifierBound γ δ

Equations

SurfaceTLAPlus.QuantifierBound.bimap f g (SurfaceTLAPlus.QuantifierBound.var ann v x_1) = SurfaceTLAPlus.QuantifierBound.var (f ann) v (g x_1)
SurfaceTLAPlus.QuantifierBound.bimap f g (SurfaceTLAPlus.QuantifierBound.vars vs x_1) = SurfaceTLAPlus.QuantifierBound.vars (Bifunctor.fst f <$> vs) (g x_1)
SurfaceTLAPlus.QuantifierBound.bimap f g (SurfaceTLAPlus.QuantifierBound.varTuple vs x_1) = SurfaceTLAPlus.QuantifierBound.varTuple (Bifunctor.fst f <$> vs) (g x_1)

Instances For

Bifunctor QuantifierBound

@[implicit_reducible]

instance SurfaceTLAPlus.instBifunctorQuantifierBound :

Equations

SurfaceTLAPlus.instBifunctorQuantifierBound = { bimap := fun {α α' β β' : Type} => SurfaceTLAPlus.QuantifierBound.bimap }

def SurfaceTLAPlus.QuantifierBound.bitraverse {G : Type → Type} [Applicative G] {α β γ δ : Type} (f : α → G γ) (g : β → G δ) :

QuantifierBound α β → G (QuantifierBound γ δ)

Equations

SurfaceTLAPlus.QuantifierBound.bitraverse f g (SurfaceTLAPlus.QuantifierBound.var ann v x_1) = (fun (x1 : γ) (x2 : δ) => SurfaceTLAPlus.QuantifierBound.var x1 v x2) <$> f ann <*> g x_1
SurfaceTLAPlus.QuantifierBound.bitraverse f g (SurfaceTLAPlus.QuantifierBound.vars vs x_1) = SurfaceTLAPlus.QuantifierBound.vars <$> traverse (bitraverse f pure) vs <*> g x_1
SurfaceTLAPlus.QuantifierBound.bitraverse f g (SurfaceTLAPlus.QuantifierBound.varTuple vs x_1) = SurfaceTLAPlus.QuantifierBound.varTuple <$> traverse (bitraverse f pure) vs <*> g x_1

Instances For

Bitraversable QuantifierBound

@[implicit_reducible]

instance SurfaceTLAPlus.instBitraversableQuantifierBound :

Equations

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

inductive SurfaceTLAPlus.IdentifierOrTuple (α : Type) :

Either a single bound variable x, or a tuple of them ⟨x, y, …, z⟩.

An inductive rather than an alias for 𝒱 ⊕ List 𝒱, for the same reason QuantifierBound is one. Expression.choose/.collect instantiate this at α × String, and α is itself a datatype being declared wherever Expression is nested inside one — Parser_/Annotations.lean's Annotation holds Expression (List Annotation). Lean's nested-inductive compiler inspects constructor argument types syntactically, and a recursive occurrence may sit under List/Prod/Sum or another inductive, but not under a definition, whose head stays opaque; reducibility does not help, an abbrev fails exactly as a def does ("contains a non valid occurrence of the datatypes being declared"). This was invisible while the element type was plain String: no α, hence no occurrence to check.

var {α : Type} (ann : α) (x : String) : IdentifierOrTuple α
tuple {α : Type} (xs : List (α × String)) : IdentifierOrTuple α

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instReprIdentifierOrTuple {α✝ : Type} [Repr α✝] :

Repr (IdentifierOrTuple α✝)

Equations

SurfaceTLAPlus.instReprIdentifierOrTuple = { reprPrec := SurfaceTLAPlus.instReprIdentifierOrTuple.repr }

def SurfaceTLAPlus.instReprIdentifierOrTuple.repr {α✝ : Type} [Repr α✝] :

IdentifierOrTuple α✝ → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instBEqIdentifierOrTuple {α✝ : Type} [BEq α✝] :

BEq (IdentifierOrTuple α✝)

Equations

SurfaceTLAPlus.instBEqIdentifierOrTuple = { beq := SurfaceTLAPlus.instBEqIdentifierOrTuple.beq }

def SurfaceTLAPlus.instBEqIdentifierOrTuple.beq {α✝ : Type} [BEq α✝] :

IdentifierOrTuple α✝ → IdentifierOrTuple α✝ → Bool

Equations

SurfaceTLAPlus.instBEqIdentifierOrTuple.beq (SurfaceTLAPlus.IdentifierOrTuple.var a a_1) (SurfaceTLAPlus.IdentifierOrTuple.var b b_1) = (a == b && a_1 == b_1)
SurfaceTLAPlus.instBEqIdentifierOrTuple.beq (SurfaceTLAPlus.IdentifierOrTuple.tuple a) (SurfaceTLAPlus.IdentifierOrTuple.tuple b) = (a == b)
SurfaceTLAPlus.instBEqIdentifierOrTuple.beq x✝¹ x✝ = false

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instDecidableEqIdentifierOrTuple {α✝ : Type} [DecidableEq α✝] :

DecidableEq (IdentifierOrTuple α✝)

Equations

SurfaceTLAPlus.instDecidableEqIdentifierOrTuple = SurfaceTLAPlus.instDecidableEqIdentifierOrTuple.decEq

def SurfaceTLAPlus.instDecidableEqIdentifierOrTuple.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : IdentifierOrTuple α✝) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
SurfaceTLAPlus.instDecidableEqIdentifierOrTuple.decEq (SurfaceTLAPlus.IdentifierOrTuple.var ann x_2) (SurfaceTLAPlus.IdentifierOrTuple.tuple xs) = isFalse ⋯
SurfaceTLAPlus.instDecidableEqIdentifierOrTuple.decEq (SurfaceTLAPlus.IdentifierOrTuple.tuple xs) (SurfaceTLAPlus.IdentifierOrTuple.var ann x_2) = isFalse ⋯
SurfaceTLAPlus.instDecidableEqIdentifierOrTuple.decEq (SurfaceTLAPlus.IdentifierOrTuple.tuple a) (SurfaceTLAPlus.IdentifierOrTuple.tuple b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instInhabitedIdentifierOrTuple {α : Type} :

Inhabited (IdentifierOrTuple α)

Independent of α — the empty tuple needs no annotation.

Equations

SurfaceTLAPlus.instInhabitedIdentifierOrTuple = { default := SurfaceTLAPlus.IdentifierOrTuple.tuple [] }

Functor IdentifierOrTuple

@[implicit_reducible]

instance SurfaceTLAPlus.instFunctorIdentifierOrTuple :

Equations

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

Traversable IdentifierOrTuple

@[implicit_reducible]

instance SurfaceTLAPlus.instTraversableIdentifierOrTuple :

Equations

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

@[reducible, inline]

abbrev SurfaceTLAPlus.CommentAnnotation :

General annotations, as supported in Apalache.

Equations

SurfaceTLAPlus.CommentAnnotation = (String × List (String ⊕ ℤ ⊕ Bool ⊕ String))

Instances For

inductive SurfaceTLAPlus.Expression (α : Type) :

TLA⁺ expressions as accepted syntactically, before desugaring. The α parameter carries whatever comment-annotation payload the caller wants attached at binder sites (e.g. @type annotations).

var {α : Type} : String → Expression α
An unqualified identifier.
opCall {α : Type} : Expression α → List (Expression α) → Expression α
An operator call f(e₁, …, eₙ).
prefixCall {α : Type} : PrefixOperator → Expression α → Expression α
infixCall {α : Type} : Expression α → InfixOperator → Expression α → Expression α
postfixCall {α : Type} : Expression α → PostfixOperator → Expression α
parens {α : Type} : Expression α → Expression α
bforall {α : Type} : List (QuantifierBound α (Expression α)) → Expression α → Expression α
Bounded universal quantification \A q \in A : e.
bexists {α : Type} : List (QuantifierBound α (Expression α)) → Expression α → Expression α
Bounded existential quantification \E q \in A : p.
forall {α : Type} : List String → Expression α → Expression α
Unbounded universal quantification \A x, y, …, z : p.
exists {α : Type} : List String → Expression α → Expression α
Unbounded existential quantification \E x, y, …, z : p.
fforall {α : Type} : List String → Expression α → Expression α
Temporal universal quantification \AA x, y, …, z : p.
eexists {α : Type} : List String → Expression α → Expression α
Temporal existential quantification \EE x, y, …, z : p.
choose {α : Type} : IdentifierOrTuple α → Option (Expression α) → Expression α → Expression α
Hilbert's epsilon operator CHOOSE x \in A : p. Each bound name carries its own annotation, the same way QuantifierBound does — a binder here is as annotatable as one in \A/\E.
set {α : Type} : List (Expression α) → Expression α
A literal set {e₁, …, eₙ}.
collect {α : Type} : IdentifierOrTuple α → Expression α → Expression α → Expression α
Set collection/filtering {x \in A : p}. Bound names carry annotations, as in choose.
map' {α : Type} : Expression α → List (QuantifierBound α (Expression α)) → Expression α
The image of a function by a set {e : x \in A}.
fnCall {α : Type} : Expression α → List (Expression α) → Expression α
A function call f[e₁, …, eₙ].
fn {α : Type} : List (QuantifierBound α (Expression α)) → Expression α → Expression α
A function literal [x \in A, …, z \in B ↦ e].
fnSet {α : Type} : Expression α → Expression α → Expression α
The set of all functions from a domain to a codomain, [A -> B].
record {α : Type} : List (α × String × Expression α) → Expression α
A literal record [a |-> e₁, …, z |-> eₙ].
recordSet {α : Type} : List (α × String × Expression α) → Expression α
The set of all records whose fields are in the given sets, [a : A, …, z : Z].
except {α : Type} : Expression α → List (List (String ⊕ List (Expression α)) × Expression α) → Expression α
Function update [f EXCEPT ![e₁] = e₂].
recordAccess {α : Type} : Expression α → String → Expression α
Record access r.x.
tuple {α : Type} : List (Expression α) → Expression α
A literal tuple <<e₁, …, eₙ>>.
if {α : Type} : Expression α → Expression α → Expression α → Expression α
Conditional IF e₁ THEN e₂ ELSE e₃.
case {α : Type} : List (Expression α × Expression α) → Option (Expression α) → Expression α
Case distinction CASE p₁ -> e₁ [] … [] OTHER -> eₙ₊₁.
conj {α : Type} : List (Expression α) → Expression α
Conjunction list /\ P /\ … /\ R.
disj {α : Type} : List (Expression α) → Expression α
Disjunction list \/ P \/ … \/ R.
nat {α : Type} : String → Expression α
str {α : Type} : String → Expression α
at {α : Type} : Expression α
@, TLA⁺'s self-reference inside EXCEPT.
true {α : Type} : Expression α
false {α : Type} : Expression α
stutter {α : Type} : Expression α → Expression α → Expression α
The stuttering-allowed action [A]_e.

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instReprExpression {α✝ : Type} [Repr α✝] :

Repr (Expression α✝)

Equations

SurfaceTLAPlus.instReprExpression = { reprPrec := SurfaceTLAPlus.instReprExpression.repr }

partial def SurfaceTLAPlus.instReprExpression.repr {α✝ : Type} [Repr α✝] :

Expression α✝ → ℕ → Std.Format

@[implicit_reducible]

instance SurfaceTLAPlus.instInhabitedExpression {a✝ : Type} :

Inhabited (Expression a✝)

Equations

SurfaceTLAPlus.instInhabitedExpression = { default := SurfaceTLAPlus.instInhabitedExpression.default }

@[implicit_reducible]

instance SurfaceTLAPlus.instBEqExpression {α✝ : Type} [BEq α✝] :

BEq (Expression α✝)

Equations

SurfaceTLAPlus.instBEqExpression = { beq := SurfaceTLAPlus.instBEqExpression.beq }

partial def SurfaceTLAPlus.instBEqExpression.beq {α✝ : Type} [BEq α✝] :

Expression α✝ → Expression α✝ → Bool

partial def SurfaceTLAPlus.Expression.map {α β : Type} (f : α → β) (e : Expression α) :

Expression β

@[implicit_reducible]

instance SurfaceTLAPlus.instFunctorExpression :

Functor Expression

Equations

SurfaceTLAPlus.instFunctorExpression = { map := fun {α β : Type} => SurfaceTLAPlus.Expression.map }

@[implicit_reducible]

def SurfaceTLAPlus.instInhabitedExpressionOfApplicative {F : Type → Type} [Applicative F] {α : Type} :

Inhabited (F (Expression α))

Equations

SurfaceTLAPlus.instInhabitedExpressionOfApplicative = { default := pure SurfaceTLAPlus.Expression.at }

Instances For

partial def SurfaceTLAPlus.Expression.traverse {F : Type → Type} [Applicative F] {α β : Type} (f : α → F β) (e : Expression α) :

F (Expression β)

@[implicit_reducible]

instance SurfaceTLAPlus.instTraversableExpression :

Traversable Expression

Equations

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

@[implicit_reducible]

instance SurfaceTLAPlus.instTraversableProd {α : Type} :

Traversable (Prod α)

Equations

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

inductive SurfaceTLAPlus.Declaration (α : Type) :

A top-level TLA⁺ declaration, prior to desugaring. Own type rather than the Core/Declaration.lean shared one CoreTLAPlus/TypedTLAPlus reuse verbatim: a function definition's binder list here may still be shared-domain (x, y \in S) or tuple-pattern (<<x,y>> \in S) sugar — the same QuantifierBound shape \A/\E/set-builders already accept — which Desugarer/TLAPlus.lean flattens down to CoreTLAPlus.Declaration.function's plain per-binder form before anything past desugaring ever sees it. RECURSIVE and module INSTANCE are not represented.

constants {α : Type} : List (String × α) → Declaration α
variables {α : Type} : List (String × α) → Declaration α
assume {α : Type} : Expression α → Declaration α
operator {α : Type} : α → String → List (String × ℕ) → Expression α → Declaration α
An operator definition, optionally with higher-order arguments. Each parameter's Nat is its arity (0 for x, 3 for F(_, _, _), …).
function {α : Type} : α → String → List (QuantifierBound α (Expression α)) → Expression α → Declaration α
A function definition. Each binder may itself be a shared-domain or tuple-pattern shorthand (QuantifierBound, same shape quantifiers accept).

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instReprDeclaration {α : Type} [Repr α] :

Repr (Declaration α)

Hand-written since deriving Repr can't discharge the higher-kinded Repr (Expression α) obligation.

Equations

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

@[implicit_reducible]

instance SurfaceTLAPlus.instFunctorDeclaration :

Functor Declaration

Equations

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

@[implicit_reducible]

instance SurfaceTLAPlus.instTraversableDeclaration :

Traversable Declaration

Equations

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

structure SurfaceTLAPlus.Module (α β : Type) :

A parsed TLA⁺ module, EXTENDS-list and all, wrapping the embedded (Distributed) PlusCal algorithm at whatever α the caller instantiates it at — kept abstract to avoid a cyclic import between the two Core ASTs. Own type for the same reason Declaration above is: its declarations₁/declarations₂ are lists of this Declaration, not Core/Declaration.lean's shared one.

name : String
extends : List String
declarations₁ : List (Declaration β)
pcalAlgorithm : Option α
declarations₂ : List (Declaration β)

Instances For

@[implicit_reducible]

instance SurfaceTLAPlus.instInhabitedModule {a✝ a✝¹ : Type} :

Inhabited (Module a✝ a✝¹)

Equations

SurfaceTLAPlus.instInhabitedModule = { default := SurfaceTLAPlus.instInhabitedModule.default }

@[implicit_reducible]

instance SurfaceTLAPlus.instReprModule {α β : Type} [Repr α] [Repr β] :

Repr (Module α β)

Hand-written, same reason as Declaration's Repr instance above.

Equations

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

@[implicit_reducible]

instance SurfaceTLAPlus.instBifunctorModule :

Bifunctor Module

@@ posOf m, for the same reason SurfacePlusCal.Process/.Algorithm's instances carry it: mapping a module rebuilds the structure, and a rebuilt node that isn't re-registered has no position of its own — posOf then answers for it with whatever unrelated value last occupied that address (Common/Position.lean).

Equations

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