Term-creation specification

This module defines the data describing how to build the term constructors for a cvc5 term kind, and the environment extension storing that data.

A specification entry is written once, in the typed form, and describes everything both layers need:

• the sort shape of each argument and of the result,
• the type and size variables the operator is polymorphic in, with their refinement classes,
• which n-ary variants to generate.

The untyped signature is derived from the typed one by erasure: every shape becomes a plain Untyped.Term. See Cvc.Gen for the generators.

inductive Cvc.SizeExpr : Type

Natural-number expression describing a sort index, such as a bit-vector size.

Size variables are bound by the enclosing OpSpec, either as a size binder or as an operator index. Arithmetic is needed by operators whose result index is computed: BITVECTOR_CONCAT sums its arguments' sizes, BITVECTOR_EXTRACT yields hi - lo + 1, BITVECTOR_REPEAT yields n * k.

Subtraction is Nat subtraction, so it truncates at zero.

• lit (n : Nat) : SizeExpr

  Literal size.

• var (name : Lean.Name) : SizeExpr

  Size variable, bound by the enclosing OpSpec.

• add (lft rgt : SizeExpr) : SizeExpr

  Sum of two sizes.

• sub (lft rgt : SizeExpr) : SizeExpr

  Truncated difference of two sizes.

• mul (lft rgt : SizeExpr) : SizeExpr

  Product of two sizes.

• arity : SizeExpr

  The operator's own arity: how many term arguments it was applied to.

  For a result whose size is not a function of its arguments' sorts but of how many there are. In the fixed-arity constructor this is a literal; in the n-ary one it is the term array's size, which makes that signature depend on a runtime value. No entry currently uses it.

@[instance_reducible]

instance Cvc.instInhabitedSizeExpr : Inhabited SizeExpr

Equations

• Cvc.instInhabitedSizeExpr = { default := Cvc.instInhabitedSizeExpr.default }

def Cvc.instReprSizeExpr.repr : SizeExpr → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cvc.instReprSizeExpr : Repr SizeExpr

Equations

• Cvc.instReprSizeExpr = { reprPrec := Cvc.instReprSizeExpr.repr }

@[instance_reducible]

instance Cvc.instBEqSizeExpr : BEq SizeExpr

Equations

• Cvc.instBEqSizeExpr = { beq := Cvc.instBEqSizeExpr.beq }

def Cvc.instBEqSizeExpr.beq : SizeExpr → SizeExpr → Bool

Equations

• Cvc.instBEqSizeExpr.beq (Cvc.SizeExpr.lit a) (Cvc.SizeExpr.lit b) = (a == b)
• Cvc.instBEqSizeExpr.beq (Cvc.SizeExpr.var a) (Cvc.SizeExpr.var b) = (a == b)
• Cvc.instBEqSizeExpr.beq (a.add a_1) (b.add b_1) = (Cvc.instBEqSizeExpr.beq a b && Cvc.instBEqSizeExpr.beq a_1 b_1)
• Cvc.instBEqSizeExpr.beq (a.sub a_1) (b.sub b_1) = (Cvc.instBEqSizeExpr.beq a b && Cvc.instBEqSizeExpr.beq a_1 b_1)
• Cvc.instBEqSizeExpr.beq (a.mul a_1) (b.mul b_1) = (Cvc.instBEqSizeExpr.beq a b && Cvc.instBEqSizeExpr.beq a_1 b_1)
• Cvc.instBEqSizeExpr.beq Cvc.SizeExpr.arity Cvc.SizeExpr.arity = true
• Cvc.instBEqSizeExpr.beq x✝¹ x✝ = false

partial def Cvc.SizeExpr.vars : SizeExpr → Array Lean.Name

Size variables occurring in a size expression.

inductive Cvc.Shape : Type

Sort shape: Typ extended with type variables and size arithmetic.

A shape describes the sort of an argument or result as the typed layer sees it. Two operations are defined on shapes:

• erasure, which forgets the shape entirely and yields the untyped signature, where every argument and the result are plain Untyped.Terms;
• rendering, which turns the shape into the Lean type indexing a Typed.Term.

• var (name : Lean.Name) : Shape

  Type variable, bound by the enclosing OpSpec.

• bool : Shape

  SMT-LIB Bool, rendered as Bool.

• int : Shape

  SMT-LIB Int, rendered as Int.

• real : Shape

  SMT-LIB Real, rendered as Rat.

• string : Shape

  SMT-LIB String, rendered as String.

• regex : Shape

  SMT-LIB RegLan, rendered as Regex.

• roundingMode : Shape

  SMT-LIB RoundingMode, rendered as Float.RoundingMode.

• bitVec (size : SizeExpr) : Shape

  SMT-LIB bit-vector, rendered as BitVec size.

• float (exp sig : SizeExpr) : Shape

  SMT-LIB floating point, rendered as Float exp sig.

• finiteField (size : SizeExpr) : Shape

  SMT-LIB finite field, rendered as FiniteField size.

• seq (elm : Shape) : Shape

  SMT-LIB sequence, rendered as Array elm.

• set (elm : Shape) : Shape

  SMT-LIB set, rendered as Set elm; requires Ord on elm.

• bag (elm : Shape) : Shape

  SMT-LIB bag, rendered as Bag elm; requires Ord on elm.

• array (idx elm : Shape) : Shape

  SMT-LIB array, rendered as TotalMap idx elm; requires Ord on idx.

• fn (dom cod : Shape) : Shape

  SMT-LIB function, rendered as the Lean arrow dom → cod.

  Curried: fn α (fn β γ) describes the SMT sort (-> α β γ).

@[instance_reducible]

instance Cvc.instInhabitedShape : Inhabited Shape

Equations

• Cvc.instInhabitedShape = { default := Cvc.instInhabitedShape.default }

@[instance_reducible]

instance Cvc.instReprShape : Repr Shape

Equations

• Cvc.instReprShape = { reprPrec := Cvc.instReprShape.repr }

def Cvc.instReprShape.repr : Shape → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cvc.instReprShape.repr Cvc.Shape.bool prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Shape.bool")).group prec✝
• Cvc.instReprShape.repr Cvc.Shape.int prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Shape.int")).group prec✝
• Cvc.instReprShape.repr Cvc.Shape.real prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Shape.real")).group prec✝
• Cvc.instReprShape.repr Cvc.Shape.string prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Shape.string")).group prec✝
• Cvc.instReprShape.repr Cvc.Shape.regex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Shape.regex")).group prec✝
• Cvc.instReprShape.repr Cvc.Shape.roundingMode prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Shape.roundingMode")).group prec✝

@[instance_reducible]

instance Cvc.instBEqShape : BEq Shape

Equations

• Cvc.instBEqShape = { beq := Cvc.instBEqShape.beq }

def Cvc.instBEqShape.beq : Shape → Shape → Bool

Equations

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

partial def Cvc.Shape.typeVars : Shape → Array Lean.Name

Type variables occurring in a shape.

partial def Cvc.Shape.sizeVars : Shape → Array Lean.Name

Size variables occurring in a shape.

partial def Cvc.Shape.ordVars : Shape → Array Lean.Name

Type variables that need an Ord instance, because they index a Set, Bag or TotalMap.

Set, Bag and TotalMap are Std.TreeSet/Std.TreeMap wrappers, so their element (respectively index) type must be ordered.

inductive Cvc.NaryUnit : Type

Unit element used by an n-ary operator's N' variant on an empty term array.

• bool (b : Bool) : NaryUnit

  Boolean literal, built with Term.mkBool.

• int (i : Int) : NaryUnit

  Integer literal, built with Term.mkInt.

@[instance_reducible]

instance Cvc.instInhabitedNaryUnit : Inhabited NaryUnit

Equations

• Cvc.instInhabitedNaryUnit = { default := Cvc.instInhabitedNaryUnit.default }

@[instance_reducible]

instance Cvc.instReprNaryUnit : Repr NaryUnit

Equations

• Cvc.instReprNaryUnit = { reprPrec := Cvc.instReprNaryUnit.repr }

def Cvc.instReprNaryUnit.repr : NaryUnit → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cvc.instBEqNaryUnit : BEq NaryUnit

Equations

• Cvc.instBEqNaryUnit = { beq := Cvc.instBEqNaryUnit.beq }

def Cvc.instBEqNaryUnit.beq : NaryUnit → NaryUnit → Bool

Equations

• Cvc.instBEqNaryUnit.beq (Cvc.NaryUnit.bool a) (Cvc.NaryUnit.bool b) = (a == b)
• Cvc.instBEqNaryUnit.beq (Cvc.NaryUnit.int a) (Cvc.NaryUnit.int b) = (a == b)
• Cvc.instBEqNaryUnit.beq x✝¹ x✝ = false

inductive Cvc.Nary : Type

Whether, and how, to generate n-ary variants of an operator.

• never : Nary

  Fixed arity only.

• array : Nary

  Also generate <id>N, taking a term array with at least two elements.

• arrayWithUnit (unit : NaryUnit) : Nary

  Also generate <id>N and <id>N', the latter defaulting on 0- and 1-element arrays.

@[instance_reducible]

instance Cvc.instInhabitedNary : Inhabited Nary

Equations

• Cvc.instInhabitedNary = { default := Cvc.instInhabitedNary.default }

@[instance_reducible]

instance Cvc.instReprNary : Repr Nary

Equations

• Cvc.instReprNary = { reprPrec := Cvc.instReprNary.repr }

def Cvc.instReprNary.repr : Nary → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cvc.instReprNary.repr Cvc.Nary.never prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Nary.never")).group prec✝
• Cvc.instReprNary.repr Cvc.Nary.array prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Nary.array")).group prec✝

def Cvc.instBEqNary.beq : Nary → Nary → Bool

Equations

• Cvc.instBEqNary.beq Cvc.Nary.never Cvc.Nary.never = true
• Cvc.instBEqNary.beq Cvc.Nary.array Cvc.Nary.array = true
• Cvc.instBEqNary.beq (Cvc.Nary.arrayWithUnit a) (Cvc.Nary.arrayWithUnit b) = (a == b)
• Cvc.instBEqNary.beq x✝¹ x✝ = false

@[instance_reducible]

instance Cvc.instBEqNary : BEq Nary

Equations

• Cvc.instBEqNary = { beq := Cvc.instBEqNary.beq }

inductive Cvc.Assoc : Type

Associativity of an infix notation.

• left : Assoc

  Left-associative: a - b - c is (a - b) - c.

• right : Assoc

  Right-associative: a ∧ b ∧ c is a ∧ (b ∧ c).

@[instance_reducible]

instance Cvc.instInhabitedAssoc : Inhabited Assoc

Equations

• Cvc.instInhabitedAssoc = { default := Cvc.instInhabitedAssoc.default }

def Cvc.instReprAssoc.repr : Assoc → Nat → Std.Format

Equations

• Cvc.instReprAssoc.repr Cvc.Assoc.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Assoc.left")).group prec✝
• Cvc.instReprAssoc.repr Cvc.Assoc.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Assoc.right")).group prec✝

@[instance_reducible]

instance Cvc.instReprAssoc : Repr Assoc

Equations

• Cvc.instReprAssoc = { reprPrec := Cvc.instReprAssoc.repr }

@[instance_reducible]

instance Cvc.instBEqAssoc : BEq Assoc

Equations

• Cvc.instBEqAssoc = { beq := Cvc.instBEqAssoc.beq }

def Cvc.instBEqAssoc.beq : Assoc → Assoc → Bool

Equations

• Cvc.instBEqAssoc.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Cvc.Notation : Type

Surface notation for an operator in the smt! DSL.

The generated grammar rule is named …smtOp.<shape>.<id>, and the expander in Cvc.Ext dispatches on the last three components of that node kind. That convention is what lets the grammar be generated per theory while the expansion logic stays written once.

• none : Notation

  No surface notation; the operator is reachable as a function only.

• pref (sym : String) (prec argPrec : Nat) : Notation

  Prefix notation such as ¬ t, with the rule's precedence and its argument's.

• inf (sym : String) (prec : Nat) (assoc : Assoc) : Notation

  Infix notation such as a ∧ b.

  When the operator also has an n-ary variant, the bracket form sym[a, b, …] is generated alongside and expands to the N function.

@[instance_reducible]

instance Cvc.instInhabitedNotation : Inhabited Notation

Equations

• Cvc.instInhabitedNotation = { default := Cvc.instInhabitedNotation.default }

def Cvc.instReprNotation.repr : Notation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cvc.instReprNotation : Repr Notation

Equations

• Cvc.instReprNotation = { reprPrec := Cvc.instReprNotation.repr }

@[instance_reducible]

instance Cvc.instBEqNotation : BEq Notation

Equations

• Cvc.instBEqNotation = { beq := Cvc.instBEqNotation.beq }

def Cvc.instBEqNotation.beq : Notation → Notation → Bool

Equations

• Cvc.instBEqNotation.beq Cvc.Notation.none Cvc.Notation.none = true
• Cvc.instBEqNotation.beq (Cvc.Notation.pref a a_1 a_2) (Cvc.Notation.pref b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Cvc.instBEqNotation.beq (Cvc.Notation.inf a a_1 a_2) (Cvc.Notation.inf b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Cvc.instBEqNotation.beq x✝¹ x✝ = false

def Cvc.Notation.sym? : Notation → Option String

The symbol of a notation, if any.

Equations

• Cvc.Notation.none.sym? = none
• (Cvc.Notation.pref a a_1 a_2).sym? = some a
• (Cvc.Notation.inf a a_1 a_2).sym? = some a

structure Cvc.ValArg : Type

A value parameter: a plain Lean argument, passed to the constructor as-is.

Constructors take data that is not a term — the Bool of a boolean literal, the String of a symbol's name, the numeral behind a bit-vector. Such a parameter is emitted unchanged in both layers, since there is no sort to erase.

• name : Lean.Name

  Name of the generated parameter.

• type : Lean.Name

  Lean type of the parameter, emitted verbatim.

@[instance_reducible]

instance Cvc.instInhabitedValArg : Inhabited ValArg

Equations

• Cvc.instInhabitedValArg = { default := Cvc.instInhabitedValArg.default }

@[instance_reducible]

instance Cvc.instReprValArg : Repr ValArg

Equations

• Cvc.instReprValArg = { reprPrec := Cvc.instReprValArg.repr }

def Cvc.instReprValArg.repr : ValArg → Nat → Std.Format

Equations

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

def Cvc.instBEqValArg.beq : ValArg → ValArg → Bool

Equations

• Cvc.instBEqValArg.beq { name := a, type := a_1 } { name := b, type := b_1 } = (a == b && a_1 == b_1)
• Cvc.instBEqValArg.beq x✝¹ x✝ = false

@[instance_reducible]

instance Cvc.instBEqValArg : BEq ValArg

Equations

• Cvc.instBEqValArg = { beq := Cvc.instBEqValArg.beq }

structure Cvc.Arg : Type

One argument of an operator.

• name : Lean.Name

  Name of the generated parameter.

• shape : Shape

  Sort shape of the argument.

@[instance_reducible]

instance Cvc.instInhabitedArg : Inhabited Arg

Equations

• Cvc.instInhabitedArg = { default := Cvc.instInhabitedArg.default }

@[instance_reducible]

instance Cvc.instReprArg : Repr Arg

Equations

• Cvc.instReprArg = { reprPrec := Cvc.instReprArg.repr }

def Cvc.instReprArg.repr : Arg → Nat → Std.Format

Equations

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

def Cvc.instBEqArg.beq : Arg → Arg → Bool

Equations

• Cvc.instBEqArg.beq { name := a, shape := a_1 } { name := b, shape := b_1 } = (a == b && a_1 == b_1)
• Cvc.instBEqArg.beq x✝¹ x✝ = false

@[instance_reducible]

instance Cvc.instBEqArg : BEq Arg

Equations

• Cvc.instBEqArg = { beq := Cvc.instBEqArg.beq }

structure Cvc.TyVar : Type

A type variable of an operator, together with the refinement classes it must satisfy.

Refinement classes are emitted as instance binders by the typed generator and dropped by the untyped one, which has no index to constrain.

• name : Lean.Name

  Name of the type variable.

• classes : Array Lean.Name

  Refinement classes, such as IsArith.

@[instance_reducible]

instance Cvc.instInhabitedTyVar : Inhabited TyVar

Equations

• Cvc.instInhabitedTyVar = { default := Cvc.instInhabitedTyVar.default }

def Cvc.instReprTyVar.repr : TyVar → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cvc.instReprTyVar : Repr TyVar

Equations

• Cvc.instReprTyVar = { reprPrec := Cvc.instReprTyVar.repr }

@[instance_reducible]

instance Cvc.instBEqTyVar : BEq TyVar

Equations

• Cvc.instBEqTyVar = { beq := Cvc.instBEqTyVar.beq }

def Cvc.instBEqTyVar.beq : TyVar → TyVar → Bool

Equations

• Cvc.instBEqTyVar.beq { name := a, classes := a_1 } { name := b, classes := b_1 } = (a == b && a_1 == b_1)
• Cvc.instBEqTyVar.beq x✝¹ x✝ = false

structure Cvc.OpSpec : Type

Everything needed to generate the typed and untyped constructors for one term kind.

The entry is keyed by id, the name of the generated function; kind is the cvc5.Kind constructor the term is built with, and is checked to exist when the entry is declared.

• id : Lean.Name

  Name of the generated function, such as and.

• kind : Lean.Name

  Constructor of cvc5.Kind, such as AND.

  For an entry built by a TermManager method this is still the kind the resulting term has, even though the term is not built by applying it.

• tmFn : Option Lean.Name

  TermManager method building the term, when it is not built by applying kind.

  Nullary constants have no mkTerm form: SET_EMPTY is mkEmptySet, PI is mkPi, and so on. Where the sort cannot be inferred from the arguments, the generated function takes one Srt per type variable the arguments leave free and builds what the method wants from those.

• sortArg : Option Shape

  Shape whose sort the tmFn method wants, when it is not the result's own.

  This does not reach the generated signature. A constructor always takes the sorts of the type variables its arguments leave free — the element sorts — and the generator builds what cvc5 asks for out of them. Most methods want the sort of the term they build; mkEmptySequence wants the element sort instead, which is what this records.

• doc : String

  Docstring of the generated fixed-arity function.

• tyVars : Array TyVar

  Type variables, with their refinement classes.

• sizeVars : Array Lean.Name

  Size variables, bound as implicit Nats and inferred from the arguments.

• indices : Array Lean.Name

  Operator indices, bound as explicit Nats ahead of the term arguments.

  An indexed operator is built by applying an Op carrying these values, rather than by applying the kind directly. They are what SMT-LIB writes as (_ extract hi lo).

• valArgs : Array ValArg

  Value parameters, in order, ahead of the term arguments.

• args : Array Arg

  Arguments, in order.

• ret : Shape

  Sort shape of the result.

• nary : Nary

  Which n-ary variants to generate.

• naryName : Option Lean.Name

  Name of the n-ary variant, when <id>N is not the right one.

  The N suffix suits an operator whose n-ary form is the same operation at greater arity. It does not suit one where the distinction is singular versus plural, a bit against several bits.

• smtNotation : Notation

  Surface notation in the smt! DSL.

• declaredIn : Lean.Name

  Module the entry was declared in, so that a generator can select a whole theory.

• order : Nat

  Declaration order, so that generated constructors come out in specification order.

@[instance_reducible]

instance Cvc.instInhabitedOpSpec : Inhabited OpSpec

Equations

• Cvc.instInhabitedOpSpec = { default := Cvc.instInhabitedOpSpec.default }

@[instance_reducible]

instance Cvc.instReprOpSpec : Repr OpSpec

Equations

• Cvc.instReprOpSpec = { reprPrec := Cvc.instReprOpSpec.repr }

def Cvc.instReprOpSpec.repr : OpSpec → Nat → Std.Format

Equations

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

def Cvc.OpSpec.ordVars (spec : OpSpec) : Array Lean.Name

Type variables that need an Ord instance, across all arguments and the result.

Equations

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

def Cvc.OpSpec.unboundRetVars (spec : OpSpec) : Array Lean.Name

Type variables occurring in the result but in no argument.

Such a variable is lost by erasure: the untyped constructor takes the result sort explicitly while the typed one recovers it from its index. Applying a kind always infers the sort from the arguments, so this is empty for every kind-built entry, and op% rejects one where it is not. It is exactly the constructors — the tmFn entries — that need it.

Equations

• spec.unboundRetVars = Array.filter (fun (x : Lean.Name) => !(Array.flatMap (fun (x : Cvc.Arg) => x.shape.typeVars) spec.args).contains x) spec.ret.typeVars

def Cvc.OpSpec.isLiftable (spec : OpSpec) : Bool

Whether the operator has a version lifted over nullables.

mkNullableLift takes a Kind and the terms to apply it to, and nothing else, which is what decides this:

• a constructor is out — it has no term argument to be null, and it builds through a TermManager method rather than a kind;
• an indexed operator is out — it is applied through an Op carrying its indices, and there is no way to hand one to mkNullableLift;
• value parameters are out for the same reason, having nowhere to go in the lifted lambda. They only ever occur on constructors, so this rules nothing else out.

Equations

• spec.isLiftable = (spec.tmFn.isNone && spec.indices.isEmpty && spec.valArgs.isEmpty && !spec.args.isEmpty)

opaque Cvc.opSpecExt : Lean.SimplePersistentEnvExtension (Lean.Name × OpSpec) (Std.HashMap Lean.Name OpSpec)

Environment extension holding every declared OpSpec, keyed by OpSpec.id.

Entries are added by the op% command and read by gen_untyped%/gen_typed%. Going through an extension is what lets the specification live in one module while generation happens in per-theory modules of both layers.

def Cvc.registerOpSpec {m : Type → Type} [Monad m] [Lean.MonadEnv m] (spec : OpSpec) : m Unit

Registers an operator specification.

Equations

• Cvc.registerOpSpec spec = Lean.modifyEnv fun (x : Lean.Environment) => Lean.PersistentEnvExtension.addEntry Cvc.opSpecExt x (spec.id, spec)

def Cvc.findOpSpec? {m : Type → Type} [Monad m] [Lean.MonadEnv m] (id : Lean.Name) : m (Option OpSpec)

Looks an operator specification up by name.

Equations

• Cvc.findOpSpec? id = do let __do_lift ← Lean.getEnv pure ((Cvc.opSpecExt.getState __do_lift).get? id)

def Cvc.opSpecCount {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m Nat

Number of registered specifications, used to stamp declaration order.

Equations

• Cvc.opSpecCount = do let __do_lift ← Lean.getEnv pure (Cvc.opSpecExt.getState __do_lift).size

def Cvc.opSpecsOf {m : Type → Type} [Monad m] [Lean.MonadEnv m] (mod : Lean.Name) : m (Array OpSpec)

Every specification declared in a module, in declaration order.

Equations

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