The op% specification command

op% declares one entry of the term-creation specification. An entry is written in the typed form and registered in Cvc.opSpecExt; nothing is generated at the declaration site.

/-- Binary conjunction. -/
op% and (lft rgt : bool) : bool := AND unit true

/-- Binary equality. -/
op% equal {α} (lft rgt : α) : bool := EQUAL unit true

/-- Binary addition. -/
op% add {α : IsArith} (lft rgt : α) : α := ADD unit 0

/-- Binary subtraction. -/
op% sub {α : IsArith} (lft rgt : α) : α := SUB nary

/-- Bit-vector concatenation. -/
op% bvConcat {n m : size} (lft : bitVec n) (rgt : bitVec m) : bitVec (n + m) := BITVECTOR_CONCAT

Binders are {α} for a plain type variable, {α : Class, …} for one constrained by refinement classes, and {n : size} for a size variable. Square brackets ahead of the binders declare operator indices, the Nats SMT-LIB writes as (_ extract hi lo):

/-- The bit range `[lo, hi]`, both bounds included. -/
op% bvExtract [hi lo] {n : size} (bv : bitVec n) : bitVec (hi - lo + 1) := BITVECTOR_EXTRACT

Indices become explicit Nat arguments ahead of the term arguments and may appear in the result's sort; size variables stay implicit and are inferred from the arguments.

Sort shapes reuse Lean's term syntax and are interpreted structurally, so no new tokens are reserved: an application head names a shape constructor (bitVec, float, finiteField, seq, set, bag, array, fn), a bare identifier is either a sort atom (bool, int, real, string, regex, roundingMode) or a variable.

The trailing nary generates the N variant, and unit <literal> generates both N and N', the latter defaulting on zero- and one-element arrays.

Syntax categories introduced here use (behavior := symbol) so that their leading identifiers are not reserved as keywords for every downstream module.

def Cvc.opIndices : Lean.ParserDescr

Operator indices, written like SMT-LIB's (_ extract hi lo).

Equations

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

def Cvc.opBinder : Lean.ParserDescr

Binder for a type or size variable.

Equations

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

def Cvc.opArgGroup : Lean.ParserDescr

Group of arguments sharing a sort shape.

Equations

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

def Cvc.opValGroup : Lean.ParserDescr

Group of value parameters sharing a Lean type, written (name :! Type).

Equations

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

def Lean.Parser.Category.opNary : Category

N-ary generation policy.

Declared with behavior := symbol so that the leading identifiers are not reserved as keywords globally, which would shadow the nary/unit field names.

Equations

• Lean.Parser.Category.opNary = { }

def Cvc.opNary.quot : Lean.ParserDescr

Equations

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

def Cvc.opNaryNary : Lean.ParserDescr

Generate the N variant, which takes a term array with at least two elements.

Equations

• Cvc.opNaryNary = Lean.ParserDescr.node `Cvc.opNaryNary 1024 (Lean.ParserDescr.nonReservedSymbol " nary" false)

def Cvc.opNaryNaryAs_ : Lean.ParserDescr

As nary, naming the variant, for when <id>N is not the right name.

Equations

• Cvc.opNaryNaryAs_ = Lean.ParserDescr.node `Cvc.opNaryNaryAs_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol " naryAs " false) (Lean.ParserDescr.const `ident))

def Cvc.opNaryUnit_ : Lean.ParserDescr

Generate the N and N' variants, the latter defaulting on 0- and 1-element arrays.

Equations

• Cvc.opNaryUnit_ = Lean.ParserDescr.node `Cvc.opNaryUnit_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol " unit " false) (Lean.ParserDescr.cat `term 0))

def Cvc.opBuild.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.opBuild : Category

How the term is built, when applying its kind is not how.

Declared with behavior := symbol so that tm is not reserved as a keyword globally.

Equations

• Lean.Parser.Category.opBuild = { }

def Cvc.opBuildTm_ : Lean.ParserDescr

Build the term with the named TermManager method rather than by applying the kind.

Equations

• Cvc.opBuildTm_ = Lean.ParserDescr.node `Cvc.opBuildTm_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol " tm " false) (Lean.ParserDescr.const `ident))

def Cvc.opBuildTmSortOf__ : Lean.ParserDescr

As tm, naming the shape whose sort the method takes, for the methods that do not take the sort of the term they build.

Equations

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

def Cvc.opNotation.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.opNotation : Category

Surface notation for the smt! DSL.

infixl/infixr/prefix are already Lean tokens, so naming them here reserves nothing new.

Equations

• Lean.Parser.Category.opNotation = { }

def Cvc.opNotationInfixl__ : Lean.ParserDescr

Left-associative infix notation, at the given precedence.

Equations

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

def Cvc.opNotationInfixr__ : Lean.ParserDescr

Right-associative infix notation, at the given precedence.

Equations

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

def Cvc.opNotationPrefix___ : Lean.ParserDescr

Prefix notation, at the given rule and argument precedences.

Equations

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

def Cvc.opStx : Lean.ParserDescr

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.

Equations

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

def Cvc.shapeAtom? : Lean.Name → Option Shape

Sort atoms, by the identifier naming them in op% syntax.

Equations

• Cvc.shapeAtom? `bool = some Cvc.Shape.bool
• Cvc.shapeAtom? `int = some Cvc.Shape.int
• Cvc.shapeAtom? `real = some Cvc.Shape.real
• Cvc.shapeAtom? `string = some Cvc.Shape.string
• Cvc.shapeAtom? `regex = some Cvc.Shape.regex
• Cvc.shapeAtom? `roundingMode = some Cvc.Shape.roundingMode
• Cvc.shapeAtom? x✝ = none

partial def Cvc.toSize (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM SizeExpr

Interprets term syntax as a size expression.

partial def Cvc.toShape (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Shape

Interprets term syntax as a sort shape.

def Cvc.toNaryUnit (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM NaryUnit

Interprets term syntax as the unit element of an n-ary operator.

Equations

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

def Cvc.elabOpStx : Lean.Elab.Command.CommandElab

Equations

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