Generating typed views

A theory's typed view is indexed by the sort it takes apart: Cvc.Typed.View.Arith : Typ → Type. It is built in two layers.

• Parts. For each sort the theory's operators produce, an inductive of those operators: View.Arith.OnBool, OnInt, OnRat, and OnAny β for those producing a type variable — ite, or add at {α : IsArith}. A constructor has its operator's indices, then the size and type variables its result does not fix, read off the kids' sorts, then implicit proofs — a type variable's classes as the Typ predicate each stands for, a computed result's equation with the part's parameter, n + m = w for a concatenation — then its kids, typed. A kid whose sort mentions a type variable is indexed by Typ.Denote of that sort.
• The theory view, one constructor per part, at the part's sort: bool (v : OnBool) : View .bool, bitVec (w) (v : OnBitVec w) : View (.bitVec w), any (v : OnAny τ.Denote) : View τ. Matching an operator refines the sort to the part's; a compound result's equation stays a proof field inside the part, so matching never unifies against anything but a sort's head.

The viewer, View.Arith.of, converts the theory's sort-erased view: that has read the kind, the kids and the indices, and the typed view adds what the sort adds — the sort fields, read off the kids, and the proofs. It answers none where it cannot: a kid whose sort no Typ describes, a sort that does not fit the operator.

• gen_typed_view% from <Spec module> generates and registers a theory's typed view.
• register_typed_view% <View> [ctor KIND, …] registers a hand-written one, whose constructors are the theory view's own.
• def.typed_term_view V — def.term_view V under open Cvc.Typed — generates the aggregate V : Typ → Type: the leaves, a variant of<Theory> per theory, other, one @[match_pattern] abbreviation per operator, a viewer V.of, and a ViewFamily instance.

Emitted names

Built with mkIdent and spliced, never written in a quotation: a name written there resolves against this module's environment, which imports neither layer.

def Cvc.TypedView.id_Cvc_Typed_View_reindex : Lean.Ident

Cvc.Typed.View.reindex.

Equations

• Cvc.TypedView.id_Cvc_Typed_View_reindex = Lean.mkIdent `Cvc.Typed.View.reindex

def Cvc.TypedView.id_Cvc_Typed_View_kids : Lean.Ident

Cvc.Typed.View.kids.

Equations

• Cvc.TypedView.id_Cvc_Typed_View_kids = Lean.mkIdent `Cvc.Typed.View.kids

def Cvc.TypedView.id_Cvc_Typed_View_typOfQ : Lean.Ident

Cvc.Typed.View.typOf?.

Equations

• Cvc.TypedView.id_Cvc_Typed_View_typOfQ = Lean.mkIdent `Cvc.Typed.View.typOf?

def Cvc.TypedView.id_Cvc_Typed_View_proofQ : Lean.Ident

Cvc.Typed.View.proof?.

Equations

• Cvc.TypedView.id_Cvc_Typed_View_proofQ = Lean.mkIdent `Cvc.Typed.View.proof?

def Cvc.TypedView.id_Cvc_Untyped_Kids_first : Lean.Ident

Cvc.Untyped.Kids.first.

Equations

• Cvc.TypedView.id_Cvc_Untyped_Kids_first = Lean.mkIdent `Cvc.Untyped.Kids.first

def Cvc.TypedView.id_Cvc_Typed_Term_relax : Lean.Ident

Cvc.Typed.Term.erase.

Equations

• Cvc.TypedView.id_Cvc_Typed_Term_relax = Lean.mkIdent `Cvc.Typed.Term.erase

def Cvc.TypedView.id_Cvc_Bag : Lean.Ident

Cvc.Bag.

Equations

• Cvc.TypedView.id_Cvc_Bag = Lean.mkIdent `Cvc.Bag

def Cvc.TypedView.id_Cvc_Env : Lean.Ident

Cvc.Env.

Equations

• Cvc.TypedView.id_Cvc_Env = Lean.mkIdent `Cvc.Env

def Cvc.TypedView.id_Cvc_FiniteField : Lean.Ident

Cvc.FiniteField.

Equations

• Cvc.TypedView.id_Cvc_FiniteField = Lean.mkIdent `Cvc.FiniteField

def Cvc.TypedView.id_Cvc_Float : Lean.Ident

Cvc.Float.

Equations

• Cvc.TypedView.id_Cvc_Float = Lean.mkIdent `Cvc.Float

def Cvc.TypedView.id_Cvc_Set : Lean.Ident

Cvc.Set.

Equations

• Cvc.TypedView.id_Cvc_Set = Lean.mkIdent `Cvc.Set

def Cvc.TypedView.id_Cvc_ToTyp : Lean.Ident

Cvc.ToTyp.

Equations

• Cvc.TypedView.id_Cvc_ToTyp = Lean.mkIdent `Cvc.ToTyp

def Cvc.TypedView.id_Cvc_TotalMap : Lean.Ident

Cvc.TotalMap.

Equations

• Cvc.TypedView.id_Cvc_TotalMap = Lean.mkIdent `Cvc.TotalMap

def Cvc.TypedView.id_Cvc_Typ : Lean.Ident

Cvc.Typ.

Equations

• Cvc.TypedView.id_Cvc_Typ = Lean.mkIdent `Cvc.Typ

def Cvc.TypedView.id_Cvc_Typ_Denote : Lean.Ident

Cvc.Typ.Denote.

Equations

• Cvc.TypedView.id_Cvc_Typ_Denote = Lean.mkIdent `Cvc.Typ.Denote

def Cvc.TypedView.id_Cvc_Typ_arrayTo : Lean.Ident

Cvc.Typ.arrayTo.

Equations

• Cvc.TypedView.id_Cvc_Typ_arrayTo = Lean.mkIdent `Cvc.Typ.arrayTo

def Cvc.TypedView.id_Cvc_Typ_bag : Lean.Ident

Cvc.Typ.bag.

Equations

• Cvc.TypedView.id_Cvc_Typ_bag = Lean.mkIdent `Cvc.Typ.bag

def Cvc.TypedView.id_Cvc_Typ_bitVec : Lean.Ident

Cvc.Typ.bitVec.

Equations

• Cvc.TypedView.id_Cvc_Typ_bitVec = Lean.mkIdent `Cvc.Typ.bitVec

def Cvc.TypedView.id_Cvc_Typ_finiteField : Lean.Ident

Cvc.Typ.finiteField.

Equations

• Cvc.TypedView.id_Cvc_Typ_finiteField = Lean.mkIdent `Cvc.Typ.finiteField

def Cvc.TypedView.id_Cvc_Typ_float : Lean.Ident

Cvc.Typ.float.

Equations

• Cvc.TypedView.id_Cvc_Typ_float = Lean.mkIdent `Cvc.Typ.float

def Cvc.TypedView.id_Cvc_Typ_function : Lean.Ident

Cvc.Typ.function.

Equations

• Cvc.TypedView.id_Cvc_Typ_function = Lean.mkIdent `Cvc.Typ.function

def Cvc.TypedView.id_Cvc_Typ_of : Lean.Ident

Cvc.Typ.of.

Equations

• Cvc.TypedView.id_Cvc_Typ_of = Lean.mkIdent `Cvc.Typ.of

def Cvc.TypedView.id_Cvc_Typ_seq : Lean.Ident

Cvc.Typ.seq.

Equations

• Cvc.TypedView.id_Cvc_Typ_seq = Lean.mkIdent `Cvc.Typ.seq

def Cvc.TypedView.id_Cvc_Typ_set : Lean.Ident

Cvc.Typ.set.

Equations

• Cvc.TypedView.id_Cvc_Typ_set = Lean.mkIdent `Cvc.Typ.set

def Cvc.TypedView.id_Cvc_TypQ_typ : Lean.Ident

Cvc.Typ?.typ.

Equations

• Cvc.TypedView.id_Cvc_TypQ_typ = Lean.mkIdent `Cvc.Typ?.typ

def Cvc.TypedView.id_Cvc_Typed_BVar : Lean.Ident

Cvc.Typed.BVar.

Equations

• Cvc.TypedView.id_Cvc_Typed_BVar = Lean.mkIdent `Cvc.Typed.BVar

def Cvc.TypedView.id_Cvc_Typed_Kids : Lean.Ident

Cvc.Typed.Kids.

Equations

• Cvc.TypedView.id_Cvc_Typed_Kids = Lean.mkIdent `Cvc.Typed.Kids

def Cvc.TypedView.id_Cvc_Typed_Term : Lean.Ident

Cvc.Typed.Term.

Equations

• Cvc.TypedView.id_Cvc_Typed_Term = Lean.mkIdent `Cvc.Typed.Term

def Cvc.TypedView.id_Cvc_Typed_Term_asBVar : Lean.Ident

Cvc.Typed.Term.asBVar.

Equations

• Cvc.TypedView.id_Cvc_Typed_Term_asBVar = Lean.mkIdent `Cvc.Typed.Term.asBVar

def Cvc.TypedView.id_Cvc_Typed_Term_getKindQ : Lean.Ident

Cvc.Typed.Term.getKind?.

Equations

• Cvc.TypedView.id_Cvc_Typed_Term_getKindQ = Lean.mkIdent `Cvc.Typed.Term.getKind?

def Cvc.TypedView.id_Cvc_Typed_Term_getSymbol : Lean.Ident

Cvc.Typed.Term.getSymbol.

Equations

• Cvc.TypedView.id_Cvc_Typed_Term_getSymbol = Lean.mkIdent `Cvc.Typed.Term.getSymbol

def Cvc.TypedView.id_cvc5_Kind_CONSTANT : Lean.Ident

cvc5.Kind.CONSTANT.

Equations

• Cvc.TypedView.id_cvc5_Kind_CONSTANT = Lean.mkIdent `cvc5.Kind.CONSTANT

def Cvc.TypedView.id_cvc5_Kind_VARIABLE : Lean.Ident

cvc5.Kind.VARIABLE.

Equations

• Cvc.TypedView.id_cvc5_Kind_VARIABLE = Lean.mkIdent `cvc5.Kind.VARIABLE

def Cvc.TypedView.id_Cvc_Typ_denoteWithOrd : Lean.Ident

Cvc.Typ.denoteWithOrd.

Equations

• Cvc.TypedView.id_Cvc_Typ_denoteWithOrd = Lean.mkIdent `Cvc.Typ.denoteWithOrd

def Cvc.TypedView.id_Cvc_Typed_ViewFamily : Lean.Ident

Cvc.Typed.ViewFamily.

Equations

• Cvc.TypedView.id_Cvc_Typed_ViewFamily = Lean.mkIdent `Cvc.Typed.ViewFamily

Sorts with a view

structure Cvc.TypedView.Head : Type

A sort a part produces, or a wrapper views.

• name : Lean.Name

  The head's name: bool, bitVec, set, …, or any for every sort.

• wrapper : String

  The wrapper's name: Bool, BitVec, Set, …, Any.

• params : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)

  The part's (and wrapper's) parameters.

• args : Array Lean.Term

  Those parameters as arguments, instances excluded.

• allArgs : Array Lean.Term

  Every parameter as an argument, a hole for each instance: what an @-application passes.

• target : Lean.Term

  The Lean type of the terms it views.

• valueKind : Option Lean.Name

  The kind of its values, which the wrapper's .value leaf reads.

• ordered : Array Lean.Name

  The parameters that carry an Ord instance.

def Cvc.TypedView.Head.plain (name : Lean.Name) (wrapper : String) (target : Lean.Name) (valueKind : Option Lean.Name) : Head

A head with no parameters.

Equations

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

def Cvc.TypedView.sizeParam (x : Lean.Ident) : Lean.MacroM (Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))

A size parameter's binder.

Equations

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

def Cvc.TypedView.typeParam (x : Lean.Ident) (ord : Bool) : Lean.MacroM (Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))

A type parameter's binders: the type, its order if a container keys on it, and its sort.

Equations

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

def Cvc.TypedView.headOf : Lean.Name → Lean.MacroM Head

The heads this prototype supports. Parameters are named apart from every specification's variables, so that a result's own variable can be unified with one.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.TypedView.headOf `bool = pure (Cvc.TypedView.Head.plain `bool "Bool" `_root_.Bool (some `CONST_BOOLEAN))
• Cvc.TypedView.headOf `int = pure (Cvc.TypedView.Head.plain `int "Int" `_root_.Int (some `CONST_INTEGER))
• Cvc.TypedView.headOf `real = pure (Cvc.TypedView.Head.plain `real "Rat" `_root_.Rat (some `CONST_RATIONAL))
• Cvc.TypedView.headOf `string = pure (Cvc.TypedView.Head.plain `string "String" `_root_.String (some `CONST_STRING))
• Cvc.TypedView.headOf `regex = pure (Cvc.TypedView.Head.plain `regex "Regex" `Cvc.Regex none)
• Cvc.TypedView.headOf `roundingMode = pure (Cvc.TypedView.Head.plain `roundingMode "RoundingMode" `Cvc.Float.RoundingMode (some `CONST_ROUNDINGMODE))
• Cvc.TypedView.headOf x✝ = Lean.Macro.throwError (toString "no view for sorts of head `" ++ toString x✝ ++ toString "`")

def Cvc.TypedView.implicitBinders (bs : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)) : Lean.MacroM (Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))

The same binders with every explicit one made implicit, for a function whose parameters are determined by its argument's type.

Equations

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

def Cvc.TypedView.shapeHead? : Shape → Option Lean.Name

The head of a result shape, if a part can be generated for it.

Equations

• Cvc.TypedView.shapeHead? Cvc.Shape.bool = some `bool
• Cvc.TypedView.shapeHead? Cvc.Shape.int = some `int
• Cvc.TypedView.shapeHead? Cvc.Shape.real = some `real
• Cvc.TypedView.shapeHead? Cvc.Shape.string = some `string
• Cvc.TypedView.shapeHead? Cvc.Shape.regex = some `regex
• Cvc.TypedView.shapeHead? Cvc.Shape.roundingMode = some `roundingMode
• Cvc.TypedView.shapeHead? (Cvc.Shape.bitVec size) = some `bitVec
• Cvc.TypedView.shapeHead? (Cvc.Shape.float exp sig) = some `float
• Cvc.TypedView.shapeHead? (Cvc.Shape.finiteField size) = some `finiteField
• Cvc.TypedView.shapeHead? elm.seq = some `seq
• Cvc.TypedView.shapeHead? elm.set = some `set
• Cvc.TypedView.shapeHead? elm.bag = some `bag
• Cvc.TypedView.shapeHead? (idx.array elm) = some `array
• Cvc.TypedView.shapeHead? (Cvc.Shape.var name) = some `any
• Cvc.TypedView.shapeHead? (dom.fn cod) = none

inductive Cvc.TypedView.Comp : Type

A component of a result that one of its head's parameters stands for.

• size (e : SizeExpr) : Comp
• type (s : Shape) : Comp

def Cvc.TypedView.resultComps (args : Array Lean.Term) : Shape → Array (Comp × Lean.Term)

What each of a head's parameters stands for in a result of that head, in parameter order.

Equations

• Cvc.TypedView.resultComps args (Cvc.Shape.bitVec e) = #[(Cvc.TypedView.Comp.size e, args[0]!)]
• Cvc.TypedView.resultComps args (Cvc.Shape.finiteField e) = #[(Cvc.TypedView.Comp.size e, args[0]!)]
• Cvc.TypedView.resultComps args (Cvc.Shape.float e s) = #[(Cvc.TypedView.Comp.size e, args[0]!), (Cvc.TypedView.Comp.size s, args[1]!)]
• Cvc.TypedView.resultComps args x_1.seq = #[(Cvc.TypedView.Comp.type x_1, args[0]!)]
• Cvc.TypedView.resultComps args x_1.set = #[(Cvc.TypedView.Comp.type x_1, args[0]!)]
• Cvc.TypedView.resultComps args x_1.bag = #[(Cvc.TypedView.Comp.type x_1, args[0]!)]
• Cvc.TypedView.resultComps args (i.array e) = #[(Cvc.TypedView.Comp.type i, args[0]!), (Cvc.TypedView.Comp.type e, args[1]!)]
• Cvc.TypedView.resultComps args (Cvc.Shape.var v) = #[(Cvc.TypedView.Comp.type (Cvc.Shape.var v), args[0]!)]
• Cvc.TypedView.resultComps args x✝ = #[]

def Cvc.TypedView.classPred? : Lean.Name → Option Lean.Name

The Typ predicate a refinement class stands for.

Equations

• Cvc.TypedView.classPred? `IsArith = some `Cvc.Typ.isArith
• Cvc.TypedView.classPred? `HasConcat = some `Cvc.Typ.hasConcat
• Cvc.TypedView.classPred? x✝ = none

Rendering kids

structure Cvc.TypedView.Roles : Type

How each variable of an entry is bound in its constructor.

• typFields : Array Lean.Name

  Type variables that are Typ fields.

• sizeFields : Array Lean.Name

  Size variables that are Nat fields, read off a kid's sort.

• subst : Array (Lean.Name × Lean.Term)

  A result variable unified with the part's parameter, and the parameter.

• ordered : Array Lean.Name

  The substituted variables whose parameter carries an Ord instance.

partial def Cvc.TypedView.renderSize (r : Roles) : SizeExpr → Except String Lean.Term

Renders a size expression, arity excluded.

partial def Cvc.TypedView.renderTyp (r : Roles) : Shape → Except String Lean.Term

Renders a shape as a Typ, type variables being Typ fields or a parameter's Typ.of.

partial def Cvc.TypedView.renderLean (r : Roles) : Shape → Except String Lean.Term

Renders a shape with no Typ field in it as the Lean type it denotes.

def Cvc.TypedView.renderKid (r : Roles) (shape : Shape) : Except String Lean.Term

The index of a kid of this shape: the denotation of its Typ if a Typ field occurs in it, which reduces once the field is matched, and the Lean type it denotes otherwise.

Equations

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

partial def Cvc.TypedView.bindIn (target : Lean.Name) (isSize : Bool) : Shape → Option Lean.Term

A pattern on a kid's Typ binding target where the shape mentions it, or none if it is not at a position a pattern can reach.

The theory views' heads

structure Cvc.TypedView.AtHead : Type

How a part's head appears in the sort-indexed view.

• fields : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)

  The theory constructor's fields ahead of the part.

• fieldArgs : Array Lean.Term

  The arguments for those fields.

• partArgs : Array (Lean.TSyntax `Lean.Parser.Term.namedArgument)

  The part's parameters, as named arguments.

• index : Lean.Term

  The sort the theory constructor is indexed by.

• pattern : Lean.Term

  A pattern on a node's sort matching the head, binding the fields.

• implicits : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)

  The abbreviations' binders standing for the fields.

• ordered : Option Lean.Ident

  The field whose denotation must be ordered, for the containers keyed on it.

def Cvc.TypedView.atHead : Lean.Name → Lean.MacroM AtHead

A part's head in the sort-indexed view.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.TypedView.atHead `bitVec = Cvc.TypedView.atHead.sizes✝ `bitVec #[`w]
• Cvc.TypedView.atHead `float = Cvc.TypedView.atHead.sizes✝ `float #[`fe, `fs]
• Cvc.TypedView.atHead `finiteField = Cvc.TypedView.atHead.sizes✝ `finiteField #[`q]
• Cvc.TypedView.atHead `seq = Cvc.TypedView.atHead.types✝ `seq #[`γ] none
• Cvc.TypedView.atHead `set = Cvc.TypedView.atHead.types✝ `set #[`γ] (some `γ)
• Cvc.TypedView.atHead `bag = Cvc.TypedView.atHead.types✝ `bag #[`γ] (some `γ)
• Cvc.TypedView.atHead `array = Cvc.TypedView.atHead.types✝ `arrayTo #[`ξ, `ζ] (some `ξ)

The registry

structure Cvc.TypedView.TypedCtor : Type

A typed view's constructor, as the aggregate's abbreviations need it.

• name : Lean.Name

  The operator's name, which its abbreviation takes.

• part : Option (Lean.Name × Lean.Name)

  For a generated view, the part holding the operator and the part's head; none for a hand-written view, whose constructors are the theory view's own.

@[instance_reducible]

instance Cvc.TypedView.instInhabitedTypedCtor : Inhabited TypedCtor

Equations

• Cvc.TypedView.instInhabitedTypedCtor = { default := Cvc.TypedView.instInhabitedTypedCtor.default }

structure Cvc.TypedView.TypedViewEntry : Type

A registered typed view.

• theory : Lean.Name

  The theory, Arith.

• view : Lean.Name

  The theory view, Cvc.Typed.View.Arith.

• ctors : Array TypedCtor

  Its operators.

• kinds : Array Lean.Name

  The kinds it takes apart.

@[instance_reducible]

instance Cvc.TypedView.instInhabitedTypedViewEntry : Inhabited TypedViewEntry

Equations

• Cvc.TypedView.instInhabitedTypedViewEntry = { default := Cvc.TypedView.instInhabitedTypedViewEntry.default }

opaque Cvc.TypedView.typedViewExt : Lean.SimplePersistentEnvExtension TypedViewEntry (Array TypedViewEntry)

The registered typed views, imported ones included.

def Cvc.TypedView.typedViews {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m (Array TypedViewEntry)

Every registered typed view.

Equations

• Cvc.TypedView.typedViews = do let __do_lift ← Lean.getEnv pure (Cvc.TypedView.typedViewExt.getState __do_lift)

A theory's typed view

structure Cvc.TypedView.GenCtor : Type

One entry's constructor in its part, and the theory viewer's alternative for it.

• ctor : Lean.TSyntax `Lean.Parser.Command.ctor
• alt : Lean.TSyntax `Lean.Parser.Term.matchAlt

def Cvc.TypedView.naryKids (spec : OpSpec) : Bool

Whether an entry's kids are an n-ary array: an n-ary entry over two arguments of one shape.

Equations

• Cvc.TypedView.naryKids spec = ((!match spec.nary with | Cvc.Nary.never => true | x => false) && spec.args.size == 2 && spec.args[0]!.shape == spec.args[1]!.shape)

def Cvc.TypedView.genCtor (spec : OpSpec) (theory untyped part : Lean.Name) (head : Head) : Lean.MacroM (Except String GenCtor)

Generates an entry's constructor in its part, and the alternative converting its sort-erased constructor — or why it cannot be. theory names the theory view, untyped the sort-erased one.

Equations

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

def Cvc.TypedView.partName (theory : Lean.Name) (head : Head) : Lean.Name

A part's name: Cvc.Typed.View.Arith.OnBool.

Equations

• Cvc.TypedView.partName theory head = theory ++ Lean.Name.mkSimple (toString "On" ++ toString head.wrapper)

def Cvc.TypedView.genTypedViewStx : Lean.ParserDescr

Generates and registers a theory's typed view from its specification module.

Equations

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

def Cvc.TypedView.elabGenTypedView : Lean.Elab.Command.CommandElab

Equations

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

def Cvc.TypedView.registerTypedViewStx : Lean.ParserDescr

Registers a hand-written typed view: its theory view, whose constructors are the operators, and each with the kind it owns. The theory is the view's last component.

Equations

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

def Cvc.TypedView.elabRegisterTypedView : Lean.Elab.Command.CommandElab

Equations

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

The typed aggregate

def Cvc.TypedView.typedTermViewStx : Lean.ParserDescr

Generates the typed aggregate V : Typ → Type from every registered typed view.

Equations

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

def Cvc.TypedView.elabTypedTermView : Lean.Elab.Command.CommandElab

Equations

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

def Cvc.Typed.«commandDef.term_view_» : Lean.ParserDescr

Declares V : Typ → Type, a term of sort τ taken apart one level, over every theory imported.

V.of τ t takes t apart; a match on the sort and the view together refines both (| .int, .add kids gives kids : Kids Int). Besides the operators, V has the leaves .value, .symbol and .bvar, and .other for a term no imported theory takes apart. Needs variable [Ω] in scope.

Equations

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