The value domain for the concrete TLA⁺ expression evaluator: Value := ZFSet, one uniform representation for every kind of TLA⁺ value.

TLA⁺ is untyped set theory, so a value — a number, a string, a set, a function, a tuple, a record — is always a set. This development represents that directly: Value is mathlib's ZFSet, set membership is ZFSet's own ∈, and the encodings below place each syntactic kind of literal into that one universe. Integers land in vtrelat/zflean's ZFSet.Int (via the ZFInt ≃+* ℤ equivalence and ZFInt.into), the booleans use its zftrue/zffalse, and functions, tuples, records and sequences are ordinary sets of ordered pairs.

Distinct kinds of value are not kept provably disjoint: FALSE and the empty set share an encoding, a string and the tuple of its code points share an encoding, and so on. TLA⁺ leaves such cross-kind comparisons unspecified, and this compiler's type checker keeps them from ever being asked — an expression of set type only evaluates against the set encodings, one of string type only against the string encoding. Only within a kind are the encodings injective.

Equality of values is not decidable — ZFSet extensionality is a ∀ — so DecidableEq/BEq are classical and noncomputable, which costs nothing here: evaluation is a Prop relation.

@[reducible, inline]

abbrev ComputableTLAPlus.Value : Type 1

A TLA⁺ value: an element of the cumulative set hierarchy. Every kind of TLA⁺ value — scalar, set, function, tuple, record — is one of these. ZFSet is Type 1 (its underlying PSet is Type), so Value is Type 1.

Equations

• ComputableTLAPlus.Value = ZFSet.{0}

noncomputable def ComputableTLAPlus.Value.ofInt (z : ℤ) : Value

The integer z, as the corresponding element of zflean's ZFSet.Int encoding. z crosses into the quotient integers ZFInt along the canonical ring equivalence ZFInt ≃+* ℤ (ZFInt.equivInt), then into ZFSet.Int along ZFInt.into. Both legs are injective with public injectivity lemmas, so ofInt is too (ofInt_inj).

Equations

• ComputableTLAPlus.Value.ofInt z = ↑(ZFSet.ZFInt.equivInt.symm z).into

noncomputable def ComputableTLAPlus.Value.ofNat (n : ℕ) : Value

The natural number n, as the integer n. TLA⁺ has one numeric type; Nat is a subset of Int, not a separate encoding.

Equations

• ComputableTLAPlus.Value.ofNat n = ComputableTLAPlus.Value.ofInt ↑n

def ComputableTLAPlus.Value.tru : Value

TRUE.

Equations

• ComputableTLAPlus.Value.tru = ZFSet.zftrue

def ComputableTLAPlus.Value.fls : Value

FALSE.

Equations

• ComputableTLAPlus.Value.fls = ZFSet.zffalse

def ComputableTLAPlus.Value.ofBool (b : Bool) : Value

The boolean b.

Equations

• ComputableTLAPlus.Value.ofBool b = bif b then ComputableTLAPlus.Value.tru else ComputableTLAPlus.Value.fls

noncomputable def ComputableTLAPlus.Value.seqGraphFrom (start : ℕ) : List Value → Value

The graph {(start, v₁), (start + 1, v₂), …} of a list of values indexed by consecutive integers from start. The shape every TLA⁺ sequence and tuple value takes.

Equations

• ComputableTLAPlus.Value.seqGraphFrom start [] = ∅
• ComputableTLAPlus.Value.seqGraphFrom start (v :: vs) = insert (ZFSet.pair (ComputableTLAPlus.Value.ofNat start) v) (ComputableTLAPlus.Value.seqGraphFrom (start + 1) vs)

noncomputable def ComputableTLAPlus.Value.ofSeq (vs : List Value) : Value

A TLA⁺ sequence or tuple ⟨v₁, …, vₙ⟩: the function {1 ↦ v₁, …, n ↦ vₙ}. Sequences and tuples are the same kind of value; their two syntactic forms differ only in how they are checked.

Equations

• ComputableTLAPlus.Value.ofSeq vs = ComputableTLAPlus.Value.seqGraphFrom 1 vs

noncomputable def ComputableTLAPlus.Value.ofTuple : List Value → Value

A TLA⁺ tuple ⟨v₁, …, vₙ⟩. Identical to ofSeq.

Equations

• ComputableTLAPlus.Value.ofTuple = ComputableTLAPlus.Value.ofSeq

noncomputable def ComputableTLAPlus.Value.ofString (s : String) : Value

A TLA⁺ string: the sequence of its Unicode code points. "abc" is the tuple ⟨97, 98, 99⟩, matching TLA⁺'s treatment of a string as a tuple of characters.

Equations

• ComputableTLAPlus.Value.ofString s = ComputableTLAPlus.Value.ofSeq (List.map (fun (c : Char) => ComputableTLAPlus.Value.ofNat c.toNat) s.toList)

noncomputable def ComputableTLAPlus.Value.recordGraph : List (String × Value) → Value

The graph {(k₁, v₁), …} of a record's fields, keyed by the string encodings of the field names.

Equations

• ComputableTLAPlus.Value.recordGraph [] = ∅
• ComputableTLAPlus.Value.recordGraph (f :: fs) = insert (ZFSet.pair (ComputableTLAPlus.Value.ofString f.1) f.2) (ComputableTLAPlus.Value.recordGraph fs)

noncomputable def ComputableTLAPlus.Value.ofRecord (fs : List (String × Value)) : Value

A TLA⁺ record [a₁ ↦ v₁, …]: the function from field-name strings to values.

Equations

• ComputableTLAPlus.Value.ofRecord fs = ComputableTLAPlus.Value.recordGraph fs

def ComputableTLAPlus.Value.ofFinSet (vs : List Value) : Value

A finite set literal {v₁, …, vₙ}.

Equations

• ComputableTLAPlus.Value.ofFinSet vs = List.foldr insert ∅ vs

@[implicit_reducible]

instance ComputableTLAPlus.Value.instInhabited : Inhabited Value

Equations

• ComputableTLAPlus.Value.instInhabited = { default := ∅ }

@[simp]

theorem ComputableTLAPlus.Value.tru_ne_fls : tru ≠ fls

TRUE and FALSE are distinct values.

@[simp]

theorem ComputableTLAPlus.Value.fls_ne_tru : fls ≠ tru

FALSE and TRUE are distinct values — the flipped orientation, for rewriting.

@[simp]

theorem ComputableTLAPlus.Value.ofBool_inj {a b : Bool} : ofBool a = ofBool b ↔ a = b

The boolean encoding is injective.

@[simp]

theorem ComputableTLAPlus.Value.ofInt_inj {a b : ℤ} : ofInt a = ofInt b ↔ a = b

The integer encoding is injective — both legs of ofInt are.

@[simp]

theorem ComputableTLAPlus.Value.ofNat_inj {m n : ℕ} : ofNat m = ofNat n ↔ m = n

The natural-number encoding is injective.

@[simp]

theorem ComputableTLAPlus.Value.mem_ofFinSet {z : Value} {vs : List Value} : z ∈ ofFinSet vs ↔ z ∈ vs

Membership in a finite set literal is list membership of the elements.

theorem ComputableTLAPlus.Value.ofInt_mem_int {k : ℤ} : ofInt k ∈ ZFSet.Int

Every integer encoding is a member of zflean's ZFSet.Int.

noncomputable def ComputableTLAPlus.Value.natSet : Value

TLA⁺'s Nat: the non-negative integers, {i ∈ Int : i ≥ 0}.

Equations

• ComputableTLAPlus.Value.natSet = ZFSet.sep (fun (z : ZFSet.{0}) => ∃ (k : ℤ), 0 ≤ k ∧ z = ComputableTLAPlus.Value.ofInt k) ZFSet.Int

@[simp]

theorem ComputableTLAPlus.Value.mem_natSet {z : Value} : z ∈ natSet ↔ ∃ (k : ℤ), 0 ≤ k ∧ z = ofInt k

Nat holds exactly the non-negative integer encodings.

noncomputable def ComputableTLAPlus.Value.intRange (a b : ℤ) : Value

The integer interval a .. b — what TLA⁺'s .. denotes. Empty when b < a. Given as an explicit finite-set literal over the enumerated integers so that it is a closed-form function of its bounds, not merely a set characterised up to extensionality.

Equations

• ComputableTLAPlus.Value.intRange a b = ComputableTLAPlus.Value.ofFinSet (List.map (fun (i : ℕ) => ComputableTLAPlus.Value.ofInt (a + ↑i)) (List.range (b + 1 - a).toNat))

@[simp]

theorem ComputableTLAPlus.Value.mem_intRange {z : Value} {a b : ℤ} : z ∈ intRange a b ↔ ∃ (k : ℤ), a ≤ k ∧ k ≤ b ∧ z = ofInt k

a .. b holds exactly the integers from a to b inclusive.

theorem ComputableTLAPlus.Value.mem_seqGraphFrom {z : Value} {start : ℕ} {vs : List Value} : z ∈ seqGraphFrom start vs ↔ ∃ (i : ℕ) (h : i < vs.length), z = ZFSet.pair (ofNat (start + i)) vs[i]

The pairs of a seqGraphFrom: one per list position, keyed by its index.

theorem ComputableTLAPlus.Value.mem_ofSeq {z : Value} {vs : List Value} : z ∈ ofSeq vs ↔ ∃ (i : ℕ) (h : i < vs.length), z = ZFSet.pair (ofNat (i + 1)) vs[i]

The pairs of a seqGraphFrom starting at 1, the sequence/tuple encoding.

theorem ComputableTLAPlus.Value.ofSeq_inj {vs ws : List Value} : ofSeq vs = ofSeq ws ↔ vs = ws

The sequence/tuple encoding is injective.

theorem ComputableTLAPlus.Value.ofSeq_isPFunc (vs : List Value) : ZFSet.IsPFunc (ofSeq vs) (intRange 1 ↑vs.length) (ofFinSet vs)

A sequence/tuple value is a partial function: {1 ↦ v₁, …, n ↦ vₙ} over the interval 1 .. n into its own elements. This is the IsPFunc witness fnApply/ZFSet.fapply needs to read a sequence at an index.

theorem ComputableTLAPlus.Value.ofSeq_isFunc (vs : List Value) : ZFSet.IsFunc (intRange 1 ↑vs.length) (ofFinSet vs) (ofSeq vs)

A sequence/tuple value is a total function from the interval 1 .. n — the IsFunc strengthening of ofSeq_isPFunc, adding that every index in range has an entry.

def ComputableTLAPlus.Value.IsSeqVal (s : Value) : Prop

s is a sequence value: a total function over some interval 1 .. n. TLA⁺'s s ∈ Seq(S) with the codomain left to ∃.

Equations

• s.IsSeqVal = ∃ (n : ℕ) (A : ComputableTLAPlus.Value), ZFSet.IsFunc (ComputableTLAPlus.Value.intRange 1 ↑n) A s

noncomputable def ComputableTLAPlus.Value.lenOf (s : Value) : ℕ

The length of a sequence value: the n for which its domain is 1 .. n. TLA⁺'s Len(s) == CHOOSE n ∈ Nat : DOMAIN s = 1 .. n. Junk off sequence values.

Equations

• s.lenOf = Classical.epsilon fun (n : ℕ) => ∃ (A : ComputableTLAPlus.Value), ZFSet.IsFunc (ComputableTLAPlus.Value.intRange 1 ↑n) A s

theorem ComputableTLAPlus.Value.isSeqVal_ofSeq (vs : List Value) : (ofSeq vs).IsSeqVal

ofSeq vs is a sequence value.

theorem ComputableTLAPlus.Value.intRange_one_inj {m n : ℕ} (h : intRange 1 ↑m = intRange 1 ↑n) : m = n

Distinct lengths give distinct index intervals over ℕ.

theorem ComputableTLAPlus.Value.isFunc_intRange_length_inj {s A B : Value} {m n : ℕ} (hm : ZFSet.IsFunc (intRange 1 ↑m) A s) (hn : ZFSet.IsFunc (intRange 1 ↑n) B s) : m = n

Two index intervals over which the same value is a total function have the same length: the value's own set of first coordinates pins the interval.

theorem ComputableTLAPlus.Value.lenOf_ofSeq (vs : List Value) : (ofSeq vs).lenOf = vs.length

lenOf (ofSeq vs) is vs.length.

noncomputable def ComputableTLAPlus.Value.cartesian (A B : Value) : Value

The TLA⁺ cartesian product A \X B: every pair <<a, b>> with a ∈ A and b ∈ B. Carved by ZFSet.sep out of the powerset that bounds the two-element tuple encodings, so it is a closed-form function of A and B, not a set fixed only up to extensionality.

Equations

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

@[simp]

theorem ComputableTLAPlus.Value.mem_cartesian {z A B : Value} : z ∈ A.cartesian B ↔ ∃ a ∈ A, ∃ b ∈ B, z = ofTuple [a, b]

A \X B holds exactly the pairs <<a, b>> with a ∈ A and b ∈ B.

theorem ComputableTLAPlus.Value.mem_recordGraph {z : Value} {fs : List (String × Value)} : z ∈ recordGraph fs ↔ ∃ (k : String) (v : Value), (k, v) ∈ fs ∧ z = ZFSet.pair (ofString k) v

The pairs of a recordGraph: one per field, keyed by the string encoding of its name.

noncomputable def ComputableTLAPlus.Value.posNatSet : Value

TLA⁺'s {n ∈ Nat : n > 0} — the strictly positive integers, Bags' codomain (Bags!IsABag's [DOMAIN B -> {n ∈ Nat : n > 0}]).

Equations

• ComputableTLAPlus.Value.posNatSet = ZFSet.sep (fun (z : ZFSet.{0}) => ∃ (k : ℤ), 0 < k ∧ z = ComputableTLAPlus.Value.ofInt k) ZFSet.Int

@[simp]

theorem ComputableTLAPlus.Value.mem_posNatSet {z : Value} : z ∈ posNatSet ↔ ∃ (k : ℤ), 0 < k ∧ z = ofInt k

{n ∈ Nat : n > 0} holds exactly the strictly positive integer encodings.

def ComputableTLAPlus.Value.IsBagVal (B : Value) : Prop

B is a bag value: a total function from some carrier set into the strictly positive integers — Bags!IsABag's own defining condition, B ∈ [DOMAIN B -> {n ∈ Nat : n > 0}].

Equations

• B.IsBagVal = ∃ (A : ComputableTLAPlus.Value), ZFSet.IsFunc A ComputableTLAPlus.Value.posNatSet B

noncomputable def ComputableTLAPlus.Value.setToBag (S : Value) : Value

Bags!SetToBag(S): the bag containing exactly one copy of every element of S, [e ∈ S ↦ 1]. Its graph is the product of S with the singleton {1} directly — ZFSet.prod's own membership characterisation already is the graph, no sep needed.

Equations

• S.setToBag = ZFSet.prod S {ComputableTLAPlus.Value.ofNat 1}

@[simp]

theorem ComputableTLAPlus.Value.mem_setToBag {z S : Value} : z ∈ S.setToBag ↔ ∃ w ∈ S, z = w.pair (ofNat 1)

SetToBag S holds exactly the pairs ⟨w, 1⟩ with w ∈ S.

noncomputable def ComputableTLAPlus.Value.rawDom (f : Value) : Value

The set of first coordinates among f's pairs — DOMAIN f without needing an IsPFunc witness first. Bounded the same way fnRead is (⋃₀ ⋃₀ f reaches every coordinate of every pair of f), so it is total on any Value, not just a genuine function graph. bagAdd/bagSub build on this rather than Value.Dom so they need no well-formedness proof to construct.

Equations

• f.rawDom = ZFSet.sep (fun (e : ZFSet.{0}) => ∃ (c : ZFSet.{0}), e.pair c ∈ f) (ZFSet.sUnion f).sUnion

@[simp]

theorem ComputableTLAPlus.Value.mem_rawDom {e f : Value} : e ∈ f.rawDom ↔ ∃ (c : ZFSet.{0}), ZFSet.pair e c ∈ f

rawDom f holds exactly the keys f pairs something with.

noncomputable def ComputableTLAPlus.Value.copiesInRaw (e f : Value) : ℕ

The multiplicity f assigns e, or 0 when f has no pair at e — CopiesIn's own "else 0" branch, as a value-level function so a sep predicate can use it directly instead of an existential disjunction. Junk (an unspecified count) only if f pairs e with something other than a single ofNat-shaped value; every genuine bag graph does not, so this only matters off IsBagVal, same convention as lenOf.

Equations

• e.copiesInRaw f = Classical.epsilon fun (n : ℕ) => ZFSet.pair e (ComputableTLAPlus.Value.ofNat n) ∈ f ∨ n = 0 ∧ e ∉ f.rawDom

theorem ComputableTLAPlus.Value.copiesInRaw_eq_zero {e f : Value} (he : e ∉ f.rawDom) : e.copiesInRaw f = 0

Off rawDom f, copiesInRaw is exactly 0 — the only n satisfying its defining disjunction's second arm, and the first is unreachable.

theorem ComputableTLAPlus.Value.IsBagVal.eq_ofNat_copiesInRaw {f : Value} (hf : f.IsBagVal) {e c : Value} (h : ZFSet.pair e c ∈ f) : c = ofNat (e.copiesInRaw f)

A genuine bag's own stored count at e is exactly what copiesInRaw computes — the IsFunc-uniqueness half of the graph-reconstruction fact bagToFun's coercion proof needs (Bag(τ) <: τ → Int is discharged as an eta-expansion through BagToSet/CopiesIn, so proving it correct means showing the eta-expanded graph reproduces the bag exactly).

theorem ComputableTLAPlus.Value.IsBagVal.mem_copiesInRaw {f : Value} (hf : f.IsBagVal) {w : Value} (hw : w ∈ f.rawDom) : ZFSet.pair w (ofNat (w.copiesInRaw f)) ∈ f

The other half: a genuine bag actually has a stored pair at every key of its domain, at exactly the count copiesInRaw computes.

theorem ComputableTLAPlus.Value.IsBagVal.mem_iff {f : Value} (hf : f.IsBagVal) {z : Value} : z ∈ f ↔ ∃ w ∈ f.rawDom, z = w.pair (ofNat (copiesInRaw w f))

A genuine bag's graph is exactly the graph copiesInRaw characterises — the self-reconstruction fact underlying bagToFun's coercion correctness (evalCoerce''s .bagToFun case): the .fn the coercion eta-expands to reproduces f exactly because f already is this graph.

noncomputable def ComputableTLAPlus.Value.bagAdd (B1 B2 : Value) : Value

Bags!(+): multiset sum, [e ∈ (DOMAIN B1) ∪ (DOMAIN B2) ↦ CopiesIn(e,B1) + CopiesIn(e,B2)]. Total on any two Values — rawDom/copiesInRaw, not Value.Dom, so no well-formedness proof is needed to build it. e ∈ rawDom B1 ∪ rawDom B2 sits inside the existential (not just the bound) so the predicate can't be satisfied by an e outside both domains with count 0 — that z genuinely is not a member, and a membership lemma stating otherwise would be false.

Equations

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

theorem ComputableTLAPlus.Value.mem_bagAdd {z B1 B2 : Value} : z ∈ B1.bagAdd B2 ↔ ∃ e ∈ B1.rawDom ∪ B2.rawDom, 0 < copiesInRaw e B1 + copiesInRaw e B2 ∧ z = e.pair (ofNat (copiesInRaw e B1 + copiesInRaw e B2))

bagAdd B1 B2 holds exactly the pairs ⟨e, c1 + c2⟩ where c1/c2 are e's count in B1/B2, e in at least one of the two domains and the sum strictly positive (sep's bound — matters only for garbage input where a stored count is itself 0; a genuine IsBagVal bag never stores one).

noncomputable def ComputableTLAPlus.Value.bagSub (B1 B2 : Value) : Value

Bags!(-): multiset difference, domain restricted to B1's, each count clamped to 0 and dropped there (ℕ's - is already truncated, so copiesInRaw e B1 - copiesInRaw e B2 is max(c1 - c2, 0); sep's codomain bound then drops the zero-count keys). Total on any two Values, same reason bagAdd is.

Equations

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

theorem ComputableTLAPlus.Value.mem_bagSub {z B1 B2 : Value} : z ∈ B1.bagSub B2 ↔ ∃ e ∈ B1.rawDom, 0 < copiesInRaw e B1 - copiesInRaw e B2 ∧ z = e.pair (ofNat (copiesInRaw e B1 - copiesInRaw e B2))

bagSub B1 B2 holds exactly the pairs ⟨e, c1 - c2⟩ (ℕ-truncated) with e ∈ rawDom B1 and the difference strictly positive.

noncomputable def ComputableTLAPlus.Value.allBagsOfSubset (B : Value) : Value

Bags!SubBag(B)'s AllBagsOfSubset (TLA⁺ book definition, not Bags.tla's own recursive one): every bag graph whose carrier is some subset of B's domain — UNION {[SB -> {n ∈ Nat : n > 0}] : SB ∈ SUBSET BagToSet(B)}. One powerset layer bounds it, since each element is itself a graph (⊆ T.prod posNatSet ⊆ (rawDom B).prod posNatSet for its own carrier T ⊆ rawDom B).

Equations

• B.allBagsOfSubset = ZFSet.sep (fun (z : ZFSet.{0}) => ∃ T ⊆ B.rawDom, ZFSet.IsFunc T ComputableTLAPlus.Value.posNatSet z) (ZFSet.prod B.rawDom ComputableTLAPlus.Value.posNatSet).powerset

theorem ComputableTLAPlus.Value.mem_allBagsOfSubset {z B : Value} : z ∈ B.allBagsOfSubset ↔ ∃ T ⊆ B.rawDom, ZFSet.IsFunc T posNatSet z

AllBagsOfSubset B holds exactly the total functions from some subset of rawDom B into the strictly positive integers.

noncomputable def ComputableTLAPlus.Value.subBag (B : Value) : Value

Bags!SubBag(B): every sub-bag of B — AllBagsOfSubset B filtered to the graphs whose count at each of its own keys is at most B's. copiesInRaw, not Value.Dom/fnApply, so no well-formedness proof is needed for B either.

Equations

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

theorem ComputableTLAPlus.Value.mem_subBag {SB B : Value} : SB ∈ B.subBag ↔ (∃ T ⊆ B.rawDom, ZFSet.IsFunc T posNatSet SB) ∧ ∀ e ∈ SB.rawDom, copiesInRaw e SB ≤ copiesInRaw e B

SubBag B holds exactly the bag graphs in AllBagsOfSubset B whose count nowhere exceeds B's own.

noncomputable def ComputableTLAPlus.Value.bagUnion (S : Value) (hS : ZFSet.IsFinite S) : Value

Bags!BagUnion(S): multiset sum across every bag of S, [e ∈ ⋃{BagToSet(B) : B ∈ S} ↦ Sum({CopiesIn(e,B) : B ∈ S})]. ⋃₀ S is already exactly "every pair from every bag of S", so its rawDom is S's combined domain directly — no separate bound construction needed. The count needs S itself finite (hS, ZFSet.IsFinite — proven correct via ZFSet.sumUpTo_insert, not a bespoke fold) to sum over; every other Bags builder is total precisely because none of the rest needs to sum across a set of bags.

Equations

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

theorem ComputableTLAPlus.Value.mem_bagUnion {z S : Value} {hS : ZFSet.IsFinite S} : z ∈ S.bagUnion hS ↔ ∃ e ∈ rawDom (ZFSet.sUnion S), 0 < hS.sum (copiesInRaw e) ∧ z = e.pair (ofNat (hS.sum (copiesInRaw e)))

bagUnion S hS holds exactly the pairs ⟨e, Σ⟩ where Σ sums e's count across every bag of S, e a key of some bag of S and the sum strictly positive.

noncomputable def ComputableTLAPlus.Value.bagCardinality (B : Value) (hB : ZFSet.IsFinite B.rawDom) : ℕ

Bags!BagCardinality(B) == Sum(B): the sum of B's own multiplicities. Same ZFSet.IsFinite.sum bagUnion's count uses, applied to one bag instead of a set of them.

Equations

• B.bagCardinality hB = hB.sum fun (x : ZFSet.{0}) => ComputableTLAPlus.Value.copiesInRaw x B

@[implicit_reducible]

instance ComputableTLAPlus.Value.instRepr : Repr Value

ZFSet carries no canonical structural pretty-printer; a value prints as an opaque placeholder. Present only so that a structure carrying a Value can still derive Repr.

Equations

• ComputableTLAPlus.Value.instRepr = { reprPrec := fun (x : ComputableTLAPlus.Value) (x_1 : ℕ) => Std.Format.text "(value : ZFSet)" }

@[implicit_reducible]

noncomputable instance ComputableTLAPlus.Value.instDecidableEq : DecidableEq Value

Value equality, classically. ZFSet equality is a universally quantified statement, so this is noncomputable — harmless, since evaluation is a Prop relation.

Equations

• a.instDecidableEq b = Classical.propDecidable (a = b)

@[implicit_reducible]

noncomputable instance ComputableTLAPlus.Value.instBEq : BEq Value

Equations

• ComputableTLAPlus.Value.instBEq = { beq := fun (a b : ComputableTLAPlus.Value) => decide (a = b) }