The target of Network2Go: the fragment of Go the thesis gives a denotational semantics to, extended with what the compilation listings actually emit.

• Blocks are List Statement, not the thesis's ; S continuation style, so var/make are ordinary statements scoped by position rather than by a syntactic continuation. Nothing in the semantics depends on the difference — a denotation folds over the list.
• Beyond the semantics' fragment: composite literals (structLit/sliceLit/mapLit/make), function literals (funcLit), and Typ.named/Typ.var. The compilation listings need Lock[struct {…}], Receiver[T], Set[T], LazyFunction[T, U], Address, Network; without them the generated code has to route around its own runtime library.
• Expression and Statement are one mutual family, parameterized by a single α (the type annotations expressions carry) rather than Statement being generic over its expression type. funcLit forces this: every callback the runtime library takes (SetFilter/SetMap/ Choose's predicates, FnConstructor/MkRecFn's generators) has a statement body, and so does the only faithful compilation of IF/CASE, Go having no conditional expression and an eager helper being wrong (IF x # 0 THEN 1/x ELSE 0 must not evaluate both arms). A Statement generic over Expr cannot tie that knot. The cost is the Bifunctor/Bitraversable pair on Statement/Function, which become Functor/Traversable over α.
• Ref is Go's own (_, x, r[e], r.x), and stays generic over Expr alone — it is not part of the mutual family, since a reference contains expressions but no statements. Unlike GuardedPlusCal.Ref it carries no type annotation, so it gets Functor/Traversable rather than the bifunctor pair.
• &&/|| are ordinary BinaryOperator cases, even though their semantics short-circuits: that is a property of their semantic rule, which case-splits on the operator regardless, not of the syntax. Splitting them out bought nothing and cost a case in every traversal.
• switch's default is a required field (the semantics always has a _ → {S} tail); select's is optional, since a blocking select with no default is exactly what the scheduling loops emit.
• Pinned at Go.Typ in ComputableGo below, the way ComputablePlusCal pins its own shared layer. This file imports nothing from Core/ — the Go AST doesn't mention TLA⁺.

inductive Go.Typ : Type

Go types, per the cases the semantics' zero value is defined over, plus named/var for the generic runtime types.

• int : Typ
• str : Typ
• bool : Typ
• chan (τ : Typ) : Typ

  chan τ

• slice (τ : Typ) : Typ

  []τ

• array (n : ℕ) (τ : Typ) : Typ

  [n]τ

• map (key value : Typ) : Typ

  map[κ]τ

• struct (fields : List (String × Typ)) : Typ

  struct {x₁ τ₁, …, xₙ τₙ}

• func (params returns : List Typ) : Typ

  func(τ₁, …, τₙ) (τ'₁, …, τ'ₘ) — parameter names aren't part of the type.

• named (name : String) (args : List Typ) : Typ

  A named type, applied to type arguments when generic: Address, Network, Lock[τ], Receiver[τ], Set[τ], LazyFunction[τ, τ'].

• var (name : String) : Typ

  A generic type parameter, bound by the enclosing Function.typeParams.

partial def Go.instReprTyp.repr : Typ → ℕ → Std.Format

@[implicit_reducible]

instance Go.instReprTyp : Repr Typ

Equations

• Go.instReprTyp = { reprPrec := Go.instReprTyp.repr }

@[implicit_reducible]

instance Go.instInhabitedTyp : Inhabited Typ

Equations

• Go.instInhabitedTyp = { default := Go.instInhabitedTyp.default }

@[implicit_reducible]

instance Go.instBEqTyp : BEq Typ

Equations

• Go.instBEqTyp = { beq := Go.instBEqTyp.beq }

partial def Go.instBEqTyp.beq : Typ → Typ → Bool

inductive Go.UnaryOperator : Type

• not : UnaryOperator

  !e

• neg : UnaryOperator

  -e

@[implicit_reducible]

instance Go.instReprUnaryOperator : Repr UnaryOperator

Equations

• Go.instReprUnaryOperator = { reprPrec := Go.instReprUnaryOperator.repr }

def Go.instReprUnaryOperator.repr : UnaryOperator → ℕ → Std.Format

Equations

• Go.instReprUnaryOperator.repr Go.UnaryOperator.not prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.UnaryOperator.not")).group prec✝
• Go.instReprUnaryOperator.repr Go.UnaryOperator.neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.UnaryOperator.neg")).group prec✝

@[implicit_reducible]

instance Go.instInhabitedUnaryOperator : Inhabited UnaryOperator

Equations

• Go.instInhabitedUnaryOperator = { default := Go.instInhabitedUnaryOperator.default }

def Go.instBEqUnaryOperator.beq : UnaryOperator → UnaryOperator → Bool

Equations

• Go.instBEqUnaryOperator.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Go.instBEqUnaryOperator : BEq UnaryOperator

Equations

• Go.instBEqUnaryOperator = { beq := Go.instBEqUnaryOperator.beq }

inductive Go.BinaryOperator : Type

Binary operators, including the short-circuiting &&/||. Their non-strictness is a fact about the semantic rule for and/or, not about the syntax, so they live here rather than as separate Expression constructors — a denotation case-splits on the operator either way.

• add : BinaryOperator
• sub : BinaryOperator
• mul : BinaryOperator
• div : BinaryOperator
• mod : BinaryOperator
• eq : BinaryOperator
• ne : BinaryOperator
• lt : BinaryOperator
• le : BinaryOperator
• gt : BinaryOperator
• ge : BinaryOperator
• and : BinaryOperator

  e₁ && e₂ — short-circuiting.

• or : BinaryOperator

  e₁ || e₂ — short-circuiting.

def Go.instReprBinaryOperator.repr : BinaryOperator → ℕ → Std.Format

Equations

• Go.instReprBinaryOperator.repr Go.BinaryOperator.add prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.add")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.sub prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.sub")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.mul prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.mul")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.div prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.div")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.mod prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.mod")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.eq")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.ne prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.ne")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.lt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.lt")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.le prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.le")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.gt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.gt")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.ge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.ge")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.and prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.and")).group prec✝
• Go.instReprBinaryOperator.repr Go.BinaryOperator.or prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.BinaryOperator.or")).group prec✝

@[implicit_reducible]

instance Go.instReprBinaryOperator : Repr BinaryOperator

Equations

• Go.instReprBinaryOperator = { reprPrec := Go.instReprBinaryOperator.repr }

@[implicit_reducible]

instance Go.instInhabitedBinaryOperator : Inhabited BinaryOperator

Equations

• Go.instInhabitedBinaryOperator = { default := Go.instInhabitedBinaryOperator.default }

@[implicit_reducible]

instance Go.instBEqBinaryOperator : BEq BinaryOperator

Equations

• Go.instBEqBinaryOperator = { beq := Go.instBEqBinaryOperator.beq }

def Go.instBEqBinaryOperator.beq : BinaryOperator → BinaryOperator → Bool

Equations

• Go.instBEqBinaryOperator.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Go.Builtin : Type

Go's builtin functions, kept out of Expression.call so that a user-chosen name colliding with one of them is a non-issue.

• len : Builtin
• cap : Builtin
• append : Builtin

@[implicit_reducible]

instance Go.instReprBuiltin : Repr Builtin

Equations

• Go.instReprBuiltin = { reprPrec := Go.instReprBuiltin.repr }

def Go.instReprBuiltin.repr : Builtin → ℕ → Std.Format

Equations

• Go.instReprBuiltin.repr Go.Builtin.len prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.Builtin.len")).group prec✝
• Go.instReprBuiltin.repr Go.Builtin.cap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.Builtin.cap")).group prec✝
• Go.instReprBuiltin.repr Go.Builtin.append prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.Builtin.append")).group prec✝

@[implicit_reducible]

instance Go.instInhabitedBuiltin : Inhabited Builtin

Equations

• Go.instInhabitedBuiltin = { default := Go.instInhabitedBuiltin.default }

def Go.instBEqBuiltin.beq : Builtin → Builtin → Bool

Equations

• Go.instBEqBuiltin.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Go.instBEqBuiltin : BEq Builtin

Equations

• Go.instBEqBuiltin = { beq := Go.instBEqBuiltin.beq }

inductive Go.Ref (Expr : Type) : Type

An assignable reference. No type annotation, unlike GuardedPlusCal.Ref.

Generic over Expr rather than a member of the Expression/Statement mutual family below: a reference contains expressions but never statements, so nothing in it needs the knot tied.

• wildcard {Expr : Type} : Ref Expr

  _

• var {Expr : Type} (name : String) : Ref Expr
• index {Expr : Type} (r : Ref Expr) (e : Expr) : Ref Expr

  r[e]

• field {Expr : Type} (r : Ref Expr) (name : String) : Ref Expr

  r.x

def Go.instReprRef.repr {Expr✝ : Type} [Repr Expr✝] : Ref Expr✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Go.instReprRef.repr Go.Ref.wildcard prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Go.Ref.wildcard")).group prec✝

@[implicit_reducible]

instance Go.instReprRef {Expr✝ : Type} [Repr Expr✝] : Repr (Ref Expr✝)

Equations

• Go.instReprRef = { reprPrec := Go.instReprRef.repr }

@[implicit_reducible]

instance Go.instInhabitedRef {a✝ : Type} : Inhabited (Ref a✝)

Equations

• Go.instInhabitedRef = { default := Go.instInhabitedRef.default }

structure Go.SelectClause (α : Type) : Type

One g → {S} arm of a select. guard is itself a statement — in practice a send or receive. Generic over the statement type so that Statement below can nest it.

• guard : α
• body : List α

@[implicit_reducible]

instance Go.instReprSelectClause {α✝ : Type} [Repr α✝] : Repr (SelectClause α✝)

Equations

• Go.instReprSelectClause = { reprPrec := Go.instReprSelectClause.repr }

def Go.instReprSelectClause.repr {α✝ : Type} [Repr α✝] : SelectClause α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Go.instInhabitedSelectClause {a✝ : Type} [Inhabited a✝] : Inhabited (SelectClause a✝)

Equations

• Go.instInhabitedSelectClause = { default := Go.instInhabitedSelectClause.default }

structure Go.SwitchClause (Expr α : Type) : Type

One v → {S} arm of a switch.

• head : Expr
• body : List α

def Go.instReprSwitchClause.repr {Expr✝ α✝ : Type} [Repr Expr✝] [Repr α✝] : SwitchClause Expr✝ α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Go.instReprSwitchClause {Expr✝ α✝ : Type} [Repr Expr✝] [Repr α✝] : Repr (SwitchClause Expr✝ α✝)

Equations

• Go.instReprSwitchClause = { reprPrec := Go.instReprSwitchClause.repr }

@[implicit_reducible]

instance Go.instInhabitedSwitchClause {a✝ : Type} [Inhabited a✝] {a✝¹ : Type} : Inhabited (SwitchClause a✝ a✝¹)

Equations

• Go.instInhabitedSwitchClause = { default := Go.instInhabitedSwitchClause.default }

inductive Go.Expression (α : Type) : Type

Go expressions, plus funcLit. α carries type annotations at the sites that need one — the same role it plays in ComputableTLAPlus.Expression.

• nat {α : Type} (n : String) : Expression α

  An integer literal, kept as its source text (same as ComputableTLAPlus.Expression.nat).

• str {α : Type} (s : String) : Expression α
• true {α : Type} : Expression α
• false {α : Type} : Expression α
• var {α : Type} (name : String) : Expression α
• unary {α : Type} (op : UnaryOperator) (e : Expression α) : Expression α
• binary {α : Type} (op : BinaryOperator) (e₁ e₂ : Expression α) : Expression α
• index {α : Type} (e i : Expression α) : Expression α

  e[i]

• field {α : Type} (e : Expression α) (name : String) : Expression α

  e.x

• call {α : Type} (f : Expression α) (args : List (Expression α)) : Expression α
• builtin {α : Type} (b : Builtin) (args : List (Expression α)) : Expression α
• structLit {α : Type} (τ : α) (fields : List (String × Expression α)) : Expression α

  τ{x₁: e₁, …} — also covers named composite literals like LazyFunction{…}.

• sliceLit {α : Type} (τ : α) (elems : List (Expression α)) : Expression α

  τ{e₁, …, eₙ}

• mapLit {α : Type} (τ : α) (entries : List (Expression α × Expression α)) : Expression α

  τ{k₁: v₁, …}

• make {α : Type} (τ : α) (args : List (Expression α)) : Expression α

  make(τ, e₁, …) — the expression form (make(map[K]V)); channel creation has its own statement, Statement.make.

• funcLit {α : Type} (params : List (String × α)) (returns : List α) (body : List (Statement α)) : Expression α

  func(x₁ τ₁, …) (τ'₁, …) { S } — an anonymous function, closing over whatever is in scope at the site it appears.

  Beyond the semantics' fragment, which has only top-level functions, but expression compilation cannot do without it: {x ∈ S : P}, {e : x ∈ S}, CHOOSE x ∈ S : P and [x ∈ S ↦ e] all compile to a runtime call taking a callback, and IF/CASE compile to an immediately-applied literal, Go having no conditional expression. Lambda-lifting these to Functions is not an alternative: they capture the enclosing block's variables, and Go has no partial application to re-supply them with.

@[implicit_reducible]

instance Go.instReprExpression {α✝ : Type} [Repr α✝] : Repr (Expression α✝)

Equations

• Go.instReprExpression = { reprPrec := Go.instReprExpression.repr_1 }

partial def Go.instReprExpression.repr_2 {α✝ : Type} [Repr α✝] : Statement α✝ → ℕ → Std.Format

@[implicit_reducible]

instance Go.instReprStatement {α✝ : Type} [Repr α✝] : Repr (Statement α✝)

Equations

• Go.instReprStatement = { reprPrec := Go.instReprStatement.repr_2 }

partial def Go.instReprStatement.repr_1 {α✝ : Type} [Repr α✝] : Expression α✝ → ℕ → Std.Format

partial def Go.instReprExpression.repr_1 {α✝ : Type} [Repr α✝] : Expression α✝ → ℕ → Std.Format

partial def Go.instReprStatement.repr_2 {α✝ : Type} [Repr α✝] : Statement α✝ → ℕ → Std.Format

inductive Go.Statement (α : Type) : Type

Go statements. Blocks are List Statement — see the module doc.

• skip {α : Type} : Statement α
• expr {α : Type} (e : Expression α) : Statement α

  A call evaluated for its effect, f(e₁, …). Go accepts only a call in this position, never an arbitrary expression, so nothing else should be built here.

  Beyond the semantics' fragment, but process compilation needs it: net.c.Send(e) and Release(ℓ, st) both return nothing, so the _ = f(…) form that covers a value-returning call is not available for them.

• print {α : Type} (e : Expression α) : Statement α
• panic {α : Type} (e : Expression α) : Statement α
• return {α : Type} (es : List (Expression α)) : Statement α

  return e₁, …, eₙ — Go's multi-valued return, widened from the semantics' single e.

• var {α : Type} (name : String) (τ : α) : Statement α

  var x τ, zero-initialized.

• assign {α : Type} (lhs : List (Ref (Expression α))) (rhs : List (Expression α)) : Statement α

  r₁, …, rₙ = e₁, …, eₘ — covers both a, b = 1, 2 and a, b = f().

• make {α : Type} (name : String) (τ : α) (capacity : Option (Expression α)) : Statement α

  c := make(chan τ, k); capacity absent means a synchronous (unbuffered) channel.

• close {α : Type} (c : Expression α) : Statement α
• send {α : Type} (c e : Expression α) : Statement α

  c <- e

• receive {α : Type} (c : Expression α) (x : Ref (Expression α)) (ok : Option (Ref (Expression α))) : Statement α

  x, ok = <-c; ok absent for the single-valued form.

• go {α : Type} (body : List (Statement α)) : Statement α
• if {α : Type} (cond : Expression α) (thenBranch elseBranch : List (Statement α)) : Statement α
• for {α : Type} (cond : Expression α) (body : List (Statement α)) : Statement α

  for e do {S} — Go's conditional loop.

• switch {α : Type} (e : Expression α) (cases : List (SwitchClause (Expression α) (Statement α))) (default : List (Statement α)) : Statement α
• select {α : Type} (cases : List (SelectClause (Statement α))) (default : Option (List (Statement α))) : Statement α

  A default-less select blocks until some guard fires.

@[implicit_reducible]

instance Go.instInhabitedExpression {α : Type} : Inhabited (Expression α)

Equations

• Go.instInhabitedExpression = { default := Go.Expression.true }

@[implicit_reducible]

instance Go.instInhabitedStatement {α : Type} : Inhabited (Statement α)

Equations

• Go.instInhabitedStatement = { default := Go.Statement.skip }

structure Go.Function (α : Type) : Type

A top-level function, plus typeParams for the generic functions the compiler emits. Each type parameter carries its constraint, which is an ordinary type: any, comparable, or one of the runtime library's own interfaces (Eq[T], Ord[T]).

• name : String
• typeParams : List (String × α)
• params : List (String × α)
• returnType : List α
• body : List (Statement α)

@[implicit_reducible]

instance Go.instReprFunction {α✝ : Type} [Repr α✝] : Repr (Function α✝)

Equations

• Go.instReprFunction = { reprPrec := Go.instReprFunction.repr }

def Go.instReprFunction.repr {α✝ : Type} [Repr α✝] : Function α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Go.instInhabitedFunction {a✝ : Type} : Inhabited (Function a✝)

Equations

• Go.instInhabitedFunction = { default := Go.instInhabitedFunction.default }

def Go.Ref.map {Expr Expr' : Type} (g : Expr → Expr') : Ref Expr → Ref Expr'

Equations

• Go.Ref.map g Go.Ref.wildcard = Go.Ref.wildcard
• Go.Ref.map g (Go.Ref.var a) = Go.Ref.var a
• Go.Ref.map g (a.index a_1) = (Go.Ref.map g a).index (g a_1)
• Go.Ref.map g (a.field a_1) = (Go.Ref.map g a).field a_1

def Go.Ref.traverse {m : Type → Type} [Applicative m] {Expr Expr' : Type} (g : Expr → m Expr') : Ref Expr → m (Ref Expr')

Equations

• Go.Ref.traverse g Go.Ref.wildcard = pure Go.Ref.wildcard
• Go.Ref.traverse g (Go.Ref.var a) = pure (Go.Ref.var a)
• Go.Ref.traverse g (a.index a_1) = Go.Ref.index <$> Go.Ref.traverse g a <*> g a_1
• Go.Ref.traverse g (a.field a_1) = (fun (x : Go.Ref Expr') => x.field a_1) <$> Go.Ref.traverse g a

@[implicit_reducible]

instance Go.instFunctorRef : Functor Ref

Equations

• Go.instFunctorRef = { map := fun {α β : Type} => Go.Ref.map }

@[implicit_reducible]

instance Go.instTraversableRef : Traversable Ref

Equations

• Go.instTraversableRef = { toFunctor := Go.instFunctorRef, traverse := fun {m : Type → Type} [Applicative m] {α β : Type} => Go.Ref.traverse }

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

partial rather than structurally recursive: α occurs under List/Prod in most constructors, the same situation Core/CorePlusCal/Syntax.lean's own instances are partial for.

partial def Go.Statement.map {α β : Type} (f : α → β) : Statement α → Statement β

@[implicit_reducible]

instance Go.instFunctorExpression : Functor Expression

Equations

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

@[implicit_reducible]

instance Go.instFunctorStatement : Functor Statement

Equations

• Go.instFunctorStatement = { map := fun {α β : Type} => Go.Statement.map }

@[implicit_reducible]

def Go.instInhabitedOfApplicative_core {F : Type u_1 → Type u_2} [Applicative F] {α : Type u_1} [Inhabited α] : Inhabited (F α)

Equations

• Go.instInhabitedOfApplicative_core = { default := pure default }

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

partial def Go.Statement.traverse {F : Type → Type} [Applicative F] {α β : Type} (f : α → F β) : Statement α → F (Statement β)

@[implicit_reducible]

instance Go.instTraversableExpression : Traversable Expression

Equations

• Go.instTraversableExpression = { toFunctor := Go.instFunctorExpression, traverse := fun {m : Type → Type} [Applicative m] {α β : Type} => Go.Expression.traverse }

@[implicit_reducible]

instance Go.instTraversableStatement : Traversable Statement

Equations

• Go.instTraversableStatement = { toFunctor := Go.instFunctorStatement, traverse := fun {m : Type → Type} [Applicative m] {α β : Type} => Go.Statement.traverse }

@[implicit_reducible]

instance Go.instFunctorFunction : Functor Function

Equations

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

@[implicit_reducible]

instance Go.instTraversableFunction : Traversable Function

Equations

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

inductive Go.Declaration (α : Type) : Type

A top-level declaration: what a generated .go file is a list of.

Function alone is enough for the statement layer, but definition compilation turns a parameter-less operator and every function definition into a package-level var — the former because Go's const accepts only a small class of types, none of which a TLA⁺ definition generally has, the latter because a function is a LazyFunction value rather than a Go func.

A package-level var cannot be generic in Go, which is what forces both forms to reject a type variable in their type; only Function carries typeParams.

• function {α : Type} (F : Function α) : Declaration α
• var {α : Type} (name : String) (τ : α) (value : Option (Expression α)) : Declaration α

  var x τ = e, with e absent for a zero-initialized declaration.

• typ {α : Type} (name : String) (τ : α) : Declaration α

  type N τ — a defined type, not an alias (type N = τ).

  Beyond the semantics' fragment, which has no top-level type declarations, but process compilation needs one: the Network struct every generated function takes a parameter of is an anonymous struct type otherwise, and Go would then require it spelled out identically at every signature that mentions it.

@[implicit_reducible]

instance Go.instReprDeclaration {α✝ : Type} [Repr α✝] : Repr (Declaration α✝)

Equations

• Go.instReprDeclaration = { reprPrec := Go.instReprDeclaration.repr }

def Go.instReprDeclaration.repr {α✝ : Type} [Repr α✝] : Declaration α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Go.instInhabitedDeclaration {a✝ : Type} : Inhabited (Declaration a✝)

Equations

• Go.instInhabitedDeclaration = { default := Go.instInhabitedDeclaration.default }

@[implicit_reducible]

instance Go.instFunctorDeclaration : Functor Declaration

Equations

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

@[implicit_reducible]

instance Go.instTraversableDeclaration : Traversable Declaration

Equations

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

@[reducible, inline]

abbrev ComputableGo.Typ : Type

Equations

• ComputableGo.Typ = Go.Typ

@[reducible, inline]

abbrev ComputableGo.Expression : Type

Equations

• ComputableGo.Expression = Go.Expression Go.Typ

@[reducible, inline]

abbrev ComputableGo.Ref : Type

Equations

• ComputableGo.Ref = Go.Ref ComputableGo.Expression

@[reducible, inline]

abbrev ComputableGo.Statement : Type

Equations

• ComputableGo.Statement = Go.Statement Go.Typ

@[reducible, inline]

abbrev ComputableGo.SelectClause : Type

Equations

• ComputableGo.SelectClause = Go.SelectClause ComputableGo.Statement

@[reducible, inline]

abbrev ComputableGo.SwitchClause : Type

Equations

• ComputableGo.SwitchClause = Go.SwitchClause ComputableGo.Expression ComputableGo.Statement

@[reducible, inline]

abbrev ComputableGo.Function : Type

Equations

• ComputableGo.Function = Go.Function Go.Typ

@[reducible, inline]

abbrev ComputableGo.Declaration : Type

Equations

• ComputableGo.Declaration = Go.Declaration Go.Typ