Sorts

The constructors of Srt, the conversions between a Srt and its Lean description Typ, and the classes IsArith and HasConcat the operators restrict their sorts with.

Function sorts are curried: α → β → γ is the sort (-> α β γ), while a function in domain position stays a higher-order argument.

def Cvc.Srt.«termLift%___» : Lean.ParserDescr

Equations

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

def Cvc.Srt.«commandDef%___:=_» : Lean.ParserDescr

Equations

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

def Cvc.Srt.bool [Ω] : EnvT BaseIO Srt

Get the Boolean sort.

Equations

• Cvc.Srt.bool = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.getBooleanSort

def Cvc.Srt.int [Ω] : EnvT BaseIO Srt

Get the Integer sort.

Equations

• Cvc.Srt.int = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.getIntegerSort

def Cvc.Srt.real [Ω] : EnvT BaseIO Srt

Get the Real sort.

Equations

• Cvc.Srt.real = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.getRealSort

def Cvc.Srt.string [Ω] : EnvT BaseIO Srt

Get the string sort.

Equations

• Cvc.Srt.string = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.getStringSort

def Cvc.Srt.regex [Ω] : EnvT BaseIO Srt

Get the regular expression sort.

Equations

• Cvc.Srt.regex = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.getRegExpSort

def Cvc.Srt.roundingMode [Ω] : EnvT BaseIO Srt

Get the rounding mode sort.

Equations

• Cvc.Srt.roundingMode = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.getRoundingModeSort

def Cvc.Srt.bitVec [Ω] (size : UInt32) : EnvT BaseIO Srt

Create a bit-vector sort.

• size The bit-width of the bit-vector sort.

Equations

• Cvc.Srt.bitVec size = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkBitVectorSort size

def Cvc.Srt.float [Ω] (exp sig : UInt32) : EnvT BaseIO Srt

Create a floating-point sort.

• exp The bit-width of the exponent of the floating-point sort.
• sig The bit-width of the significand of the floating-point sort.

Equations

• Cvc.Srt.float exp sig = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFloatingPointSort exp sig

def Cvc.Srt.finiteField [Ω] (size : Nat) : Env Srt

The sort of the finite field with size elements, size being prime.

Equations

• Cvc.Srt.finiteField size = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFiniteFieldSort size

def Cvc.Srt.ofName [Ω] (name : String) : Env Srt

The sort declared under name in this scope, failing if there is none.

Equations

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

def Cvc.Srt.isDeclared [Ω] (name : String) : Env Bool

Whether a sort has been declared under a name in this scope.

Equations

• Cvc.Srt.isDeclared name = do let __do_lift ← Cvc.getRegisteredSort?✝ name pure __do_lift.isSome

def Cvc.Srt.checkFreshSortSymbol [Ω] (symbol : String) : Env Unit

Fails if a sort named symbol has already been declared in this scope.

Equations

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

def Cvc.Srt.arrayTo [Ω] (idx elm : Srt) : EnvT BaseIO Srt

Creates the sort of arrays from idx to elm, e.g. idx.arrayTo elm.

Equations

• idx.arrayTo elm = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkArraySort idx elm

def Cvc.Srt.arrayFrom [Ω] (elm idx : Srt) : EnvT BaseIO Srt

Creates the sort of arrays to elm from idx, e.g. elm.arrayFrom idx.

Equations

• elm.arrayFrom idx = idx.arrayTo elm

def Cvc.Srt.array [Ω] (elm : Srt) : Env Srt

An array of elm-values indexed by int-values.

Equations

• elm.array = Cvc.Srt.int >>= elm.arrayFrom

def Cvc.Srt.bag [Ω] (elm : Srt) : Env Srt

The sort of bags of elm.

Equations

• elm.bag = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkBagSort elm

def Cvc.Srt.set [Ω] (elm : Srt) : Env Srt

The sort of sets of elm.

Equations

• elm.set = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkSetSort elm

def Cvc.Srt.seq [Ω] (elm : Srt) : Env Srt

The sort of sequences of elm.

Equations

• elm.seq = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkSequenceSort elm

def Cvc.Srt.tuple [Ω] (sorts : Array Srt) : Env Srt

The sort of tuples of the given components.

Equations

• Cvc.Srt.tuple sorts = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTupleSort sorts

def Cvc.Srt.function [Ω] (dom : Array Srt) (cod : Srt) (domNonempty : 0 < dom.size := by (try grind) <;> fail "failed to prove the domain is nonempty") : Env Srt

The sort of functions from the domain sorts dom to cod.

Equations

• Cvc.Srt.function dom cod domNonempty = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFunctionSort dom cod

def Cvc.Srt.abstract [Ω] (a : Abstract) : Env Srt

The abstract sort of a family, its parameters left unspecified.

Equations

• Cvc.Srt.abstract a = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkAbstractSort a.toKind

def Cvc.Srt.any [Ω] : Env Srt

cvc5's fully abstract sort, ?.

cvc5 accepts it only as a set, bag or sequence element, an array's index or element, or a function's codomain.

Equations

• Cvc.Srt.any = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkAbstractSort cvc5.SortKind.ABSTRACT_SORT

def Cvc.Srt.Abstract.toSrt [Ω] (a : Abstract) : Env Srt

Equations

• a.toSrt = Cvc.Srt.abstract a

Further constructors

def Cvc.Srt.predicate [Ω] (doms : Srts) : Env Srt

The sort of predicates over doms: functions from them to Bool.

Equations

• Cvc.Srt.predicate doms = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkPredicateSort doms

def Cvc.Srt.nullable [Ω] (elm : Srt) : Env Srt

The sort of nullable elm values, denoted Lean-side by Option.

Equations

• elm.nullable = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableSort elm

def Cvc.Srt.record [Ω] (fields : Array (String × Srt)) : Env Srt

A record sort, of named fields in order.

Fails on an empty record and on a repeated field name. The order is part of the sort: {a : Int, b : Bool} and {b : Bool, a : Int} are different.

Equations

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

def Cvc.Srt.param [Ω] (symbol : String) : Env Srt

Create a sort parameter.

• symbol The name of the sort.

Warning: This function is experimental and may change in future versions.

Equations

• Cvc.Srt.param symbol = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkParamSort symbol

def Cvc.Srt.uninterpreted [Ω] (symbol : String) : Env Srt

A new uninterpreted sort named symbol, which Typ.uninterpreted symbol then names.

The name must not be taken by another sort declared in this scope.

Equations

• Cvc.Srt.uninterpreted symbol = do Cvc.Srt.checkFreshSortSymbol symbol let u ← Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkUninterpretedSort symbol Cvc.registerSort✝ symbol u pure u

def Cvc.Srt.finiteFieldOfString [Ω] (size : String) (base : UInt32 := 10) : Env Srt

A finite field sort whose size is given in the base base.

Equations

• Cvc.Srt.finiteFieldOfString size base = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkFiniteFieldSortOfString size base

def Cvc.Srt.uninterpretedConstructor [Ω] (arity : Nat) (symbol : String) : Env Srt

An uninterpreted sort constructor, which arity parameters instantiate into a sort.

The name must not be taken by another sort declared in this scope.

Equations

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

def Cvc.Srt.unresolvedDatatype [Ω] (symbol : String) (arity : Nat := 0) : Env Srt

A placeholder for a datatype sort not yet resolved.

For mutually recursive parametric datatypes, whose declarations mention each other.

Equations

• Cvc.Srt.unresolvedDatatype symbol arity = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkUnresolvedDatatypeSort symbol arity

Datatype sorts

A datatype sort comes from a Datatype.Decl. Each call makes a fresh sort, even from an identical declaration, so a datatype is declared once per scope and then named with Typ.datatype.

def Cvc.Srt.datatype [Ω] (decl : Datatype.Decl) : Env Srt

The sort of the datatype decl declares, which Typ.datatype then names.

The datatype's name must not be taken by another sort declared in this scope.

Equations

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

def Cvc.Srt.datatypes [Ω] (decls : Array Datatype.Decl) : Env Srts

The sorts of a mutually recursive group of datatypes, declared together.

Members refer to each other through Datatype.Ctor.Decl.addSelectorUnresolved. As for Srt.datatype, each name must be new to this scope.

Equations

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

Testers

Which family a sort belongs to. Each is the guard on the accessors of that family below: asking a non-array for its index sort fails, and these are how to know not to.

def Cvc.Srt.«commandIs%_:=_» : Lean.ParserDescr

Equations

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

def Cvc.Srt.isBool [Ω] : Srt → Bool

Determine if this is the Boolean sort (SMT-LIB: Bool).

Equations

• srt✝.isBool = (Cvc.Srt.toUnsafe✝ srt✝).isBoolean

def Cvc.Srt.isInt [Ω] : Srt → Bool

Determine if this is the Integer sort (SMT-LIB: Int).

Equations

• srt✝.isInt = (Cvc.Srt.toUnsafe✝ srt✝).isInteger

def Cvc.Srt.isReal [Ω] : Srt → Bool

Determine if this is the Real sort (SMT-LIB: Real).

Equations

• srt✝.isReal = (Cvc.Srt.toUnsafe✝ srt✝).isReal

def Cvc.Srt.isString [Ω] : Srt → Bool

Determine if this is the String sort (SMT-LIB: String).

Equations

• srt✝.isString = (Cvc.Srt.toUnsafe✝ srt✝).isString

def Cvc.Srt.isRegex [Ω] : Srt → Bool

Determine if this is the regular expression sort (SMT-LIB: RegLan).

Equations

• srt✝.isRegex = (Cvc.Srt.toUnsafe✝ srt✝).isRegExp

def Cvc.Srt.isRoundingMode [Ω] : Srt → Bool

Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).

Equations

• srt✝.isRoundingMode = (Cvc.Srt.toUnsafe✝ srt✝).isRoundingMode

def Cvc.Srt.isBitVec [Ω] : Srt → Bool

Determine if this is a bit-vector sort (SMT-LIB: (_ BitVec i)).

Equations

• srt✝.isBitVec = (Cvc.Srt.toUnsafe✝ srt✝).isBitVector

def Cvc.Srt.isFloat [Ω] : Srt → Bool

Determine if this is a floating-point sort (SMT-LIB: (_ FloatingPoint eb sb)).

Equations

• srt✝.isFloat = (Cvc.Srt.toUnsafe✝ srt✝).isFloatingPoint

def Cvc.Srt.isFiniteField [Ω] : Srt → Bool

Determine if this is a finite field sort.

Equations

• srt✝.isFiniteField = (Cvc.Srt.toUnsafe✝ srt✝).isFiniteField

def Cvc.Srt.isArray [Ω] : Srt → Bool

Determine if this is an array sort.

Equations

• srt✝.isArray = (Cvc.Srt.toUnsafe✝ srt✝).isArray

def Cvc.Srt.isSet [Ω] : Srt → Bool

Determine if this is a Set sort.

Equations

• srt✝.isSet = (Cvc.Srt.toUnsafe✝ srt✝).isSet

def Cvc.Srt.isBag [Ω] : Srt → Bool

Determine if this is a Bag sort.

Equations

• srt✝.isBag = (Cvc.Srt.toUnsafe✝ srt✝).isBag

def Cvc.Srt.isSeq [Ω] : Srt → Bool

Determine if this is a Sequence sort.

Equations

• srt✝.isSeq = (Cvc.Srt.toUnsafe✝ srt✝).isSequence

def Cvc.Srt.isTuple [Ω] : Srt → Bool

Determine if this is a tuple sort.

Equations

• srt✝.isTuple = (Cvc.Srt.toUnsafe✝ srt✝).isTuple

def Cvc.Srt.isNullable [Ω] : Srt → Bool

Determine if this is a nullable sort.

Equations

• srt✝.isNullable = (Cvc.Srt.toUnsafe✝ srt✝).isNullable

def Cvc.Srt.isRecord [Ω] : Srt → Bool

Determine if this is a record sort.

Warning: this function is experimental and may change in future versions.

Equations

• srt✝.isRecord = (Cvc.Srt.toUnsafe✝ srt✝).isRecord

def Cvc.Srt.isFunction [Ω] : Srt → Bool

Determine if this is a function sort.

Equations

• srt✝.isFunction = (Cvc.Srt.toUnsafe✝ srt✝).isFunction

def Cvc.Srt.isPredicate [Ω] : Srt → Bool

Determine if this is a predicate sort.

A predicate sort is a function sort that maps to the Boolean sort. All predicate sorts are also function sorts.

Equations

• srt✝.isPredicate = (Cvc.Srt.toUnsafe✝ srt✝).isPredicate

def Cvc.Srt.isAbstract [Ω] : Srt → Bool

Determine if this is an abstract sort.

Equations

• srt✝.isAbstract = (Cvc.Srt.toUnsafe✝ srt✝).isAbstract

def Cvc.Srt.isDatatype [Ω] : Srt → Bool

Determine if this is a datatype sort.

Equations

• srt✝.isDatatype = (Cvc.Srt.toUnsafe✝ srt✝).isDatatype

def Cvc.Srt.isDatatypeConstructor [Ω] : Srt → Bool

Determine if this is a datatype constructor sort.

Equations

• srt✝.isDatatypeConstructor = (Cvc.Srt.toUnsafe✝ srt✝).isDatatypeConstructor

def Cvc.Srt.isDatatypeSelector [Ω] : Srt → Bool

Determine if this is a datatype selector sort.

Equations

• srt✝.isDatatypeSelector = (Cvc.Srt.toUnsafe✝ srt✝).isDatatypeSelector

def Cvc.Srt.isDatatypeTester [Ω] : Srt → Bool

Determine if this is a datatype tester sort.

Equations

• srt✝.isDatatypeTester = (Cvc.Srt.toUnsafe✝ srt✝).isDatatypeTester

def Cvc.Srt.isDatatypeUpdater [Ω] : Srt → Bool

Determine if this is a datatype updater sort.

Equations

• srt✝.isDatatypeUpdater = (Cvc.Srt.toUnsafe✝ srt✝).isDatatypeUpdater

def Cvc.Srt.isUninterpreted [Ω] : Srt → Bool

Determine if this is an uninterpreted sort.

Equations

• srt✝.isUninterpreted = (Cvc.Srt.toUnsafe✝ srt✝).isUninterpretedSort

def Cvc.Srt.isUninterpretedSortConstructor [Ω] : Srt → Bool

Determine if this is an uninterpreted sort constructor.

An uninterpreted sort constructor has arity > 0 and can be instantiated to construct uninterpreted sorts with given sort parameters.

Equations

• srt✝.isUninterpretedSortConstructor = (Cvc.Srt.toUnsafe✝ srt✝).isUninterpretedSortConstructor

def Cvc.Srt.isInstantiated [Ω] (srt : Srt) : Bool

Whether this sort instantiates a parametric datatype or an uninterpreted sort constructor.

cvc5 also answers true for a datatype sort without parameters: a non-empty getInstantiatedParameters is the reliable test. See Srt.instantiate.

Equations

• srt.isInstantiated = (Cvc.Srt.toUnsafe✝ srt).isInstantiated

Accessors

Each answers only for the family its tester identifies, so each comes in two forms: the plain one fails elsewhere, the ?-suffixed one answers none.

def Cvc.Srt.«commandGet%_:_:=_» : Lean.ParserDescr

Equations

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

Any sort

def Cvc.Srt.getKind? [Ω] : Srt → Option SortKind

Get the kind of this sort.

Equations

• srt✝.getKind? = (Cvc.Srt.toUnsafe✝ srt✝).getKind?

def Cvc.Srt.getKind [Ω] : Srt → Res SortKind

Get the kind of this sort.

Equations

• srt✝.getKind = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getKind

def Cvc.Srt.hasSymbol [Ω] (srt : Srt) : Res Bool

Whether this sort has a symbol, a name; see getSymbol.

Equations

• srt.hasSymbol = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt).hasSymbol

def Cvc.Srt.hasSymbol? [Ω] (srt : Srt) : Option Bool

Whether this sort has a symbol, a name; see getSymbol.

Equations

• srt.hasSymbol? = (Cvc.Srt.toUnsafe✝ srt).hasSymbol?

def Cvc.Srt.getSymbol [Ω] (srt : Srt) : Res String

The symbol of this sort, its name.

It is the name given to Srt.uninterpreted, Srt.uninterpretedConstructor or Srt.unresolvedDatatype.

Equations

• srt.getSymbol = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt).getSymbol

def Cvc.Srt.getSymbol? [Ω] (srt : Srt) : Option String

The symbol of this sort, its name.

It is the name given to Srt.uninterpreted, Srt.uninterpretedConstructor or Srt.unresolvedDatatype.

Equations

• srt.getSymbol? = (Cvc.Srt.toUnsafe✝ srt).getSymbol?

Sized and parameterized sorts

def Cvc.Srt.getBitVecSize [Ω] : Srt → Res UInt32

The bit-width of the bit-vector sort.

Equations

• srt✝.getBitVecSize = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getBitVectorSize

def Cvc.Srt.getBitVecSize? [Ω] : Srt → Option UInt32

The bit-width of the bit-vector sort.

Equations

• srt✝.getBitVecSize? = (Cvc.Srt.toUnsafe✝ srt✝).getBitVectorSize?

def Cvc.Srt.getFiniteFieldSize [Ω] : Srt → Res Nat

The size of the finite field sort.

Equations

• srt✝.getFiniteFieldSize = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getFiniteFieldSize

def Cvc.Srt.getFiniteFieldSize? [Ω] : Srt → Option Nat

The size of the finite field sort.

Equations

• srt✝.getFiniteFieldSize? = (Cvc.Srt.toUnsafe✝ srt✝).getFiniteFieldSize?

def Cvc.Srt.getFloatExponentSize? [Ω] : Srt → Option UInt32

The bit-width of the exponent of the floating-point sort.

Equations

• srt✝.getFloatExponentSize? = (Cvc.Srt.toUnsafe✝ srt✝).getFloatingPointExponentSize?

def Cvc.Srt.getFloatExponentSize [Ω] : Srt → Res UInt32

The bit-width of the exponent of the floating-point sort.

Equations

• srt✝.getFloatExponentSize = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getFloatingPointExponentSize

def Cvc.Srt.getFloatSignificandSize [Ω] : Srt → Res UInt32

The width of the significand of the floating-point sort.

Equations

• srt✝.getFloatSignificandSize = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getFloatingPointSignificandSize

def Cvc.Srt.getFloatSignificandSize? [Ω] : Srt → Option UInt32

The width of the significand of the floating-point sort.

Equations

• srt✝.getFloatSignificandSize? = (Cvc.Srt.toUnsafe✝ srt✝).getFloatingPointSignificandSize?

Containers

def Cvc.Srt.getArrayIndexSort [Ω] (srt : Srt) : Res Srt

The index sort of an array sort.

Equations

• srt.getArrayIndexSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt).getArrayIndexSort

def Cvc.Srt.getArrayIndexSort? [Ω] (srt : Srt) : Option Srt

The index sort of an array sort.

Equations

• srt.getArrayIndexSort? = (Cvc.Srt.toUnsafe✝ srt).getArrayIndexSort?

def Cvc.Srt.getArrayElementSort [Ω] (srt : Srt) : Res Srt

The element sort of an array sort.

Equations

• srt.getArrayElementSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt).getArrayElementSort

def Cvc.Srt.getArrayElementSort? [Ω] (srt : Srt) : Option Srt

The element sort of an array sort.

Equations

• srt.getArrayElementSort? = (Cvc.Srt.toUnsafe✝ srt).getArrayElementSort?

def Cvc.Srt.getSetElementSort? [Ω] : Srt → Option Srt

The element sort of a set sort.

Equations

• srt✝.getSetElementSort? = (Cvc.Srt.toUnsafe✝ srt✝).getSetElementSort?

def Cvc.Srt.getSetElementSort [Ω] : Srt → Res Srt

The element sort of a set sort.

Equations

• srt✝.getSetElementSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getSetElementSort

def Cvc.Srt.getBagElementSort? [Ω] : Srt → Option Srt

The element sort of a bag sort.

Equations

• srt✝.getBagElementSort? = (Cvc.Srt.toUnsafe✝ srt✝).getBagElementSort?

def Cvc.Srt.getBagElementSort [Ω] : Srt → Res Srt

The element sort of a bag sort.

Equations

• srt✝.getBagElementSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getBagElementSort

def Cvc.Srt.getSeqElementSort [Ω] : Srt → Res Srt

The element sort of a sequence sort.

Equations

• srt✝.getSeqElementSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getSequenceElementSort

def Cvc.Srt.getSeqElementSort? [Ω] : Srt → Option Srt

The element sort of a sequence sort.

Equations

• srt✝.getSeqElementSort? = (Cvc.Srt.toUnsafe✝ srt✝).getSequenceElementSort?

def Cvc.Srt.getNullableElementSort [Ω] : Srt → Res Srt

The element sort of a nullable sort.

Equations

• srt✝.getNullableElementSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getNullableElementSort

def Cvc.Srt.getNullableElementSort? [Ω] : Srt → Option Srt

The element sort of a nullable sort.

Equations

• srt✝.getNullableElementSort? = (Cvc.Srt.toUnsafe✝ srt✝).getNullableElementSort?

def Cvc.Srt.getTupleLength? [Ω] : Srt → Option UInt32

The length of a tuple sort.

Equations

• srt✝.getTupleLength? = (Cvc.Srt.toUnsafe✝ srt✝).getTupleLength?

def Cvc.Srt.getTupleLength [Ω] : Srt → Res UInt32

The length of a tuple sort.

Equations

• srt✝.getTupleLength = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getTupleLength

def Cvc.Srt.getTupleSorts? [Ω] : Srt → Option Srts

The element sorts of a tuple sort.

Equations

• srt✝.getTupleSorts? = (Cvc.Srt.toUnsafe✝ srt✝).getTupleSorts?

def Cvc.Srt.getTupleSorts [Ω] : Srt → Res Srts

The element sorts of a tuple sort.

Equations

• srt✝.getTupleSorts = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getTupleSorts

Functions

def Cvc.Srt.getFunctionArity [Ω] : Srt → Res Nat

The arity of a function sort.

Equations

• srt✝.getFunctionArity = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getFunctionArity

def Cvc.Srt.getFunctionArity? [Ω] : Srt → Option Nat

The arity of a function sort.

Equations

• srt✝.getFunctionArity? = (Cvc.Srt.toUnsafe✝ srt✝).getFunctionArity?

def Cvc.Srt.getFunctionDomainSorts [Ω] : Srt → Res Srts

The domain sorts of a function sort.

Equations

• srt✝.getFunctionDomainSorts = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getFunctionDomainSorts

def Cvc.Srt.getFunctionDomainSorts? [Ω] : Srt → Option Srts

The domain sorts of a function sort.

Equations

• srt✝.getFunctionDomainSorts? = (Cvc.Srt.toUnsafe✝ srt✝).getFunctionDomainSorts?

def Cvc.Srt.getFunctionCodomainSort [Ω] : Srt → Res Srt

The codomain sort of a function sort.

Equations

• srt✝.getFunctionCodomainSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getFunctionCodomainSort

def Cvc.Srt.getFunctionCodomainSort? [Ω] : Srt → Option Srt

The codomain sort of a function sort.

Equations

• srt✝.getFunctionCodomainSort? = (Cvc.Srt.toUnsafe✝ srt✝).getFunctionCodomainSort?

Abstract and uninterpreted sorts

def Cvc.Srt.getAbstractedKind [Ω] : Srt → Res SortKind

The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.

Equations

• srt✝.getAbstractedKind = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getAbstractedKind

def Cvc.Srt.getAbstractedKind? [Ω] : Srt → Option SortKind

The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.

Equations

• srt✝.getAbstractedKind? = (Cvc.Srt.toUnsafe✝ srt✝).getAbstractedKind?

def Cvc.Srt.getUninterpretedSortConstructor [Ω] : Srt → Res Srt

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

Equations

• srt✝.getUninterpretedSortConstructor = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getUninterpretedSortConstructor

def Cvc.Srt.getUninterpretedSortConstructor? [Ω] : Srt → Option Srt

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

Equations

• srt✝.getUninterpretedSortConstructor? = (Cvc.Srt.toUnsafe✝ srt✝).getUninterpretedSortConstructor?

def Cvc.Srt.getUninterpretedSortConstructorArity? [Ω] : Srt → Option UInt32

The arity of an uninterpreted sort constructor sort.

Equations

• srt✝.getUninterpretedSortConstructorArity? = (Cvc.Srt.toUnsafe✝ srt✝).getUninterpretedSortConstructorArity?

def Cvc.Srt.getUninterpretedSortConstructorArity [Ω] : Srt → Res UInt32

The arity of an uninterpreted sort constructor sort.

Equations

• srt✝.getUninterpretedSortConstructorArity = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getUninterpretedSortConstructorArity

def Cvc.Srt.getInstantiatedParameters [Ω] (srt : Srt) : Res Srts

The sorts a parametric datatype or an uninterpreted sort constructor was instantiated with.

See Srt.instantiate.

Equations

• srt.getInstantiatedParameters = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt).getInstantiatedParameters

def Cvc.Srt.getInstantiatedParameters? [Ω] (srt : Srt) : Option Srts

The sorts a parametric datatype or an uninterpreted sort constructor was instantiated with.

See Srt.instantiate.

Equations

• srt.getInstantiatedParameters? = (Cvc.Srt.toUnsafe✝ srt).getInstantiatedParameters?

Datatypes

The datatype sorts: what a constructor, selector or tester sort relates. The Datatype they answer has its own API, in Cvc.Untyped.Theory.Datatype.

def Cvc.Srt.getDatatype? [Ω] : Srt → Option Datatype

Get the underlying datatype of a datatype sort.

Equations

• srt✝.getDatatype? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatype?

def Cvc.Srt.getDatatype [Ω] : Srt → Res Datatype

Get the underlying datatype of a datatype sort.

Equations

• srt✝.getDatatype = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatype

def Cvc.Srt.getDatatypeArity [Ω] : Srt → Res Nat

Get the arity of a datatype sort.

Number of type parameters if the datatype is parametric, 0 otherwise.

Equations

• srt✝.getDatatypeArity = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeArity

def Cvc.Srt.getDatatypeArity? [Ω] : Srt → Option Nat

Get the arity of a datatype sort.

Number of type parameters if the datatype is parametric, 0 otherwise.

Equations

• srt✝.getDatatypeArity? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeArity?

def Cvc.Srt.getDatatypeConstructorArity [Ω] : Srt → Res Nat

The arity of a datatype constructor sort.

Equations

• srt✝.getDatatypeConstructorArity = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeConstructorArity

def Cvc.Srt.getDatatypeConstructorArity? [Ω] : Srt → Option Nat

The arity of a datatype constructor sort.

Equations

• srt✝.getDatatypeConstructorArity? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeConstructorArity?

def Cvc.Srt.getDatatypeConstructorDomainSorts? [Ω] : Srt → Option Srts

The domain sorts of a datatype constructor sort.

Equations

• srt✝.getDatatypeConstructorDomainSorts? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeConstructorDomainSorts?

def Cvc.Srt.getDatatypeConstructorDomainSorts [Ω] : Srt → Res Srts

The domain sorts of a datatype constructor sort.

Equations

• srt✝.getDatatypeConstructorDomainSorts = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeConstructorDomainSorts

def Cvc.Srt.getDatatypeConstructorCodomainSort [Ω] : Srt → Res Srt

The codomain sort of a constructor sort.

Equations

• srt✝.getDatatypeConstructorCodomainSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeConstructorCodomainSort

def Cvc.Srt.getDatatypeConstructorCodomainSort? [Ω] : Srt → Option Srt

The codomain sort of a constructor sort.

Equations

• srt✝.getDatatypeConstructorCodomainSort? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeConstructorCodomainSort?

def Cvc.Srt.getDatatypeSelectorDomainSort [Ω] : Srt → Res Srt

The domain sort of a datatype selector sort.

Equations

• srt✝.getDatatypeSelectorDomainSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeSelectorDomainSort

def Cvc.Srt.getDatatypeSelectorDomainSort? [Ω] : Srt → Option Srt

The domain sort of a datatype selector sort.

Equations

• srt✝.getDatatypeSelectorDomainSort? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeSelectorDomainSort?

def Cvc.Srt.getDatatypeSelectorCodomainSort? [Ω] : Srt → Option Srt

The codomain sort of a datatype selector sort.

Equations

• srt✝.getDatatypeSelectorCodomainSort? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeSelectorCodomainSort?

def Cvc.Srt.getDatatypeSelectorCodomainSort [Ω] : Srt → Res Srt

The codomain sort of a datatype selector sort.

Equations

• srt✝.getDatatypeSelectorCodomainSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeSelectorCodomainSort

def Cvc.Srt.getDatatypeTesterDomainSort [Ω] : Srt → Res Srt

The domain sort of a datatype tester sort.

Equations

• srt✝.getDatatypeTesterDomainSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeTesterDomainSort

def Cvc.Srt.getDatatypeTesterDomainSort? [Ω] : Srt → Option Srt

The domain sort of a datatype tester sort.

Equations

• srt✝.getDatatypeTesterDomainSort? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeTesterDomainSort?

def Cvc.Srt.getDatatypeTesterCodomainSort [Ω] : Srt → Res Srt

The codomain sort of a datatype tester sort.

Equations

• srt✝.getDatatypeTesterCodomainSort = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeTesterCodomainSort

def Cvc.Srt.getDatatypeTesterCodomainSort? [Ω] : Srt → Option Srt

The codomain sort of a datatype tester sort.

Equations

• srt✝.getDatatypeTesterCodomainSort? = (Cvc.Srt.toUnsafe✝ srt✝).getDatatypeTesterCodomainSort?

Instantiation and substitution

def Cvc.Srt.instantiate [Ω] (srt : Srt) (params : Srts) : Res Srt

Instantiates a parametric sort with the given parameters.

Equations

• srt.instantiate params = Except.mapError Cvc.Error.ofUnsafe✝ ((Cvc.Srt.toUnsafe✝ srt).instantiate params)

def Cvc.Srt.instantiate? [Ω] (srt : Srt) (params : Srts) : Option Srt

Instantiates a parametric sort with the given parameters.

Equations

• srt.instantiate? params = (Cvc.Srt.toUnsafe✝ srt).instantiate? params

def Cvc.Srt.substitute [Ω] (srt : Srt) (srts replacements : Srts) : Res Srt

Replaces srts by replacements throughout a sort, simultaneously.

Equations

• srt.substitute srts replacements = Except.mapError Cvc.Error.ofUnsafe✝ ((Cvc.Srt.toUnsafe✝ srt).substitute srts replacements)

def Cvc.Srt.substitute? [Ω] (srt : Srt) (srts replacements : Srts) : Option Srt

Replaces srts by replacements throughout a sort, simultaneously.

Equations

• srt.substitute? srts replacements = (Cvc.Srt.toUnsafe✝ srt).substitute? srts replacements

Sort refinements

@[reducible, inline]

abbrev Cvc.Typ.isArith : Typ → Bool

Whether a sort is arithmetic: Int or Real.

Equations

• Cvc.Typ.int.isArith = true
• Cvc.Typ.real.isArith = true
• Cvc.Typ.bool.isArith = false
• Cvc.Typ.string.isArith = false
• Cvc.Typ.regex.isArith = false
• Cvc.Typ.roundingMode.isArith = false
• (Cvc.Typ.bitVec size).isArith = false
• (Cvc.Typ.float exp sig).isArith = false
• (Cvc.Typ.finiteField size).isArith = false
• (Cvc.Typ.arrayTo idx elm).isArith = false
• (Cvc.Typ.bag elm).isArith = false
• (Cvc.Typ.set elm).isArith = false
• (Cvc.Typ.seq elm).isArith = false
• (Cvc.Typ.prod args).isArith = false
• elm.nullable.isArith = false
• (Cvc.Typ.record fields).isArith = false
• (Cvc.Typ.datatype name).isArith = false
• (dom.function cod).isArith = false
• (Cvc.Typ.uninterpreted name).isArith = false

theorem Cvc.Typ.typs_of_isArith {typ : Typ} : typ.isArith = true → typ = int ∨ typ = real

@[reducible, inline]

abbrev Cvc.Typ.hasConcat : Typ → Bool

Whether a sort has concatenation: strings and sequences.

Equations

• Cvc.Typ.string.hasConcat = true
• (Cvc.Typ.seq elm).hasConcat = true
• Cvc.Typ.int.hasConcat = false
• Cvc.Typ.real.hasConcat = false
• Cvc.Typ.bool.hasConcat = false
• Cvc.Typ.regex.hasConcat = false
• Cvc.Typ.roundingMode.hasConcat = false
• (Cvc.Typ.bitVec size).hasConcat = false
• (Cvc.Typ.float exp sig).hasConcat = false
• (Cvc.Typ.finiteField size).hasConcat = false
• (Cvc.Typ.arrayTo idx elm).hasConcat = false
• (Cvc.Typ.bag elm).hasConcat = false
• (Cvc.Typ.set elm).hasConcat = false
• (Cvc.Typ.prod args).hasConcat = false
• elm.nullable.hasConcat = false
• (Cvc.Typ.record fields).hasConcat = false
• (Cvc.Typ.datatype name).hasConcat = false
• (dom.function cod).hasConcat = false
• (Cvc.Typ.uninterpreted name).hasConcat = false

theorem Cvc.Typ.typs_of_hasConcat {typ : Typ} : typ.hasConcat = true → typ = string ∨ ∃ (t : Typ?), typ = seq t

Conversions between Typ and Srt

def Cvc.Typ.toSrt [Ω] : Typ → Env Srt

The sort a Typ describes.

Fails only on a datatype or uninterpreted name no sort was declared under in this scope.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Typ.bool.toSrt = Cvc.Srt.bool
• Cvc.Typ.int.toSrt = Cvc.Srt.int
• Cvc.Typ.real.toSrt = Cvc.Srt.real
• Cvc.Typ.regex.toSrt = Cvc.Srt.regex
• Cvc.Typ.string.toSrt = Cvc.Srt.string
• Cvc.Typ.roundingMode.toSrt = Cvc.Srt.roundingMode
• (Cvc.Typ.bitVec size).toSrt = Cvc.Srt.bitVec size.toUInt32
• (Cvc.Typ.float exp sig).toSrt = Cvc.Srt.float exp.toUInt32 sig.toUInt32
• (Cvc.Typ.finiteField size).toSrt = Cvc.Srt.finiteField size
• (Cvc.Typ.arrayTo idx elm).toSrt = do let __do_lift ← elm.toSrt let __do_lift_1 ← idx.toSrt __do_lift_1.arrayTo __do_lift
• (Cvc.Typ.bag elm).toSrt = elm.toSrt >>= Cvc.Srt.bag
• (Cvc.Typ.set elm).toSrt = elm.toSrt >>= Cvc.Srt.set
• (Cvc.Typ.seq elm).toSrt = elm.toSrt >>= Cvc.Srt.seq
• elm.nullable.toSrt = elm.toSrt >>= Cvc.Srt.nullable
• (Cvc.Typ.prod args).toSrt = Cvc.Typ.toSrtList args >>= Cvc.Srt.tuple
• (Cvc.Typ.record fields).toSrt = Cvc.Typ.toSrtFields fields >>= Cvc.Srt.record
• (Cvc.Typ.datatype name).toSrt = Cvc.Srt.ofName name

def Cvc.Typ.toSrtList [Ω] : List Typ → Env (Array Srt)

The sort a Typ describes.

Fails only on a datatype or uninterpreted name no sort was declared under in this scope.

Equations

• Cvc.Typ.toSrtList [] = pure #[]
• Cvc.Typ.toSrtList (hd :: tl) = do let __do_lift ← hd.toSrt let __do_lift_1 ← Cvc.Typ.toSrtList tl pure (#[__do_lift] ++ __do_lift_1)

def Cvc.Typ.toSrtFields [Ω] : List (String × Typ) → Env (Array (String × Srt))

The sort a Typ describes.

Fails only on a datatype or uninterpreted name no sort was declared under in this scope.

Equations

• Cvc.Typ.toSrtFields [] = pure #[]
• Cvc.Typ.toSrtFields ((name, ty) :: tl) = do let __do_lift ← ty.toSrt let __do_lift_1 ← Cvc.Typ.toSrtFields tl pure (#[(name, __do_lift)] ++ __do_lift_1)

def Cvc.Typ?.toSrt [Ω] : Typ? → Env Srt

The sort a Typ describes.

Fails only on a datatype or uninterpreted name no sort was declared under in this scope.

Equations

• (Cvc.Typ?.typ t).toSrt = t.toSrt
• Cvc.Typ?.any.toSrt = Cvc.Srt.any
• (Cvc.Typ?.abstract a).toSrt = Cvc.Srt.abstract a

partial def Cvc.Srt.toTyp [Ω] (srt : Srt) : Env Typ

Conversion to Typ, the inverse of Typ.toSrt wherever a Typ can describe the sort.

A function sort comes back curried, (-> α β γ) as function α (function β γ). A declared sort — a datatype or an uninterpreted sort — converts only if it is the sort this scope registered under its name.

Sorts that no Typ describes fail rather than approximate: the abstract sorts, which toTyp? accepts, instantiated parametric datatypes, uninterpreted sort constructors and their instantiations, and the datatype-operator sorts.

partial def Cvc.Srt.toTyp? [Ω] (srt : Srt) : Env Typ?

Conversion to Typ?, which unlike toTyp accepts the abstract sorts.

@[reducible, inline]

abbrev Cvc.Typ.of (α : Type) [A : ToTyp α] : Typ

The Typ associated to some type.

Equations

• Cvc.Typ.of α = Cvc.ToTyp.typ α

@[reducible, inline]

abbrev Cvc.ToTyp.srt [Ω] {α : Type} [ToTyp α] : Env Srt

The sort a type denotes, through its ToTyp instance.

Equations

• Cvc.ToTyp.srt = (Cvc.Typ.of α).toSrt

@[reducible, inline]

abbrev Cvc.Srt.of [Ω] (α : Type) [A : ToTyp α] : Env Srt

The sort a type denotes, through its ToTyp instance.

Equations

• Cvc.Srt.of α = Cvc.ToTyp.srt

@[instance_reducible, instance 100]

instance Cvc.instOrdRat : Ord Rat

The usual order on rationals, which core lacks; at low priority, so that Mathlib's wins.

Equations

• Cvc.instOrdRat = { compare := fun (x y : Rat) => compareOfLessAndEq x y }

@[instance_reducible]

instance Cvc.ToTyp.instBool : ToTyp Bool

Equations

• Cvc.ToTyp.instBool = { typ := Cvc.Typ.bool }

@[instance_reducible]

instance Cvc.ToTyp.instInt : ToTyp Int

Equations

• Cvc.ToTyp.instInt = { typ := Cvc.Typ.int }

@[instance_reducible]

instance Cvc.ToTyp.instRat : ToTyp Rat

Equations

• Cvc.ToTyp.instRat = { typ := Cvc.Typ.real }

@[instance_reducible]

instance Cvc.ToTyp.instString : ToTyp String

Equations

• Cvc.ToTyp.instString = { typ := Cvc.Typ.string }

@[instance_reducible]

instance Cvc.ToTyp.instBitVec {size : Nat} : ToTyp (BitVec size)

Equations

• Cvc.ToTyp.instBitVec = { typ := Cvc.Typ.bitVec size }

@[instance_reducible]

instance Cvc.ToTyp.instRoundingMode : ToTyp Float.RoundingMode

Equations

• Cvc.ToTyp.instRoundingMode = { typ := Cvc.Typ.roundingMode }

@[instance_reducible]

instance Cvc.ToTyp.instArray {α : Type} [A : ToTyp α] : ToTyp (Array α)

Lean's Array denotes cvc5's sequences; SMT-LIB arrays are TotalMap.

Equations

• Cvc.ToTyp.instArray = { typ := Cvc.Typ.seq (Cvc.Typ?.typ (Cvc.ToTyp.typ α)) }

@[instance_reducible]

instance Cvc.ToTyp.instOption {α : Type} [A : ToTyp α] : ToTyp (Option α)

Lean's Option denotes cvc5's Nullable.

Equations

• Cvc.ToTyp.instOption = { typ := (Cvc.ToTyp.typ α).nullable }

class Cvc.IsArith (α : Type) [A : ToTyp α] : Prop

α denotes an arithmetic sort: Int or Rat.

• valid_typ : (ToTyp.typ α).isArith = true

  Proof that α's Typ is arithmetic.

instance Cvc.instIsArithInt : IsArith Int

instance Cvc.instIsArithRat : IsArith Rat

class Cvc.HasConcat (α : Type) [A : ToTyp α] : Prop

α denotes a sort with concatenation: String or Array _.

• valid_typ : (ToTyp.typ α).hasConcat = true

  Proof that α's Typ has concatenation.

instance Cvc.instHasConcatString : HasConcat String

instance Cvc.instHasConcatArray {α : Type} [ToTyp α] : HasConcat (Array α)

Regular expressions

structure Cvc.Regex : Type

The Lean type indexing regular-expression terms; it carries no data.

@[instance_reducible]

instance Cvc.instDecidableEqRegex : DecidableEq Regex

Equations

• Cvc.instDecidableEqRegex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.instHashableRegex.hash : Regex → UInt64

Equations

• Cvc.instHashableRegex.hash { } = 0

@[instance_reducible]

instance Cvc.instHashableRegex : Hashable Regex

Equations

• Cvc.instHashableRegex = { hash := Cvc.instHashableRegex.hash }

def Cvc.instOrdRegex.ord : Regex → Regex → Ordering

Equations

• Cvc.instOrdRegex.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance Cvc.instOrdRegex : Ord Regex

Equations

• Cvc.instOrdRegex = { compare := Cvc.instOrdRegex.ord }

@[instance_reducible]

instance Cvc.Regex.instToTyp : ToTyp Regex

Equations

• Cvc.Regex.instToTyp = { typ := Cvc.Typ.regex }

Functions

@[instance_reducible]

instance Cvc.ToTyp.instForall {α β : Type} [A : ToTyp α] [B : ToTyp β] : ToTyp (α → β)

Equations

• Cvc.ToTyp.instForall = { typ := (Cvc.ToTyp.typ α).function (Cvc.Typ?.typ (Cvc.ToTyp.typ β)) }

A sort written either way

Where the sort-erased DSL lets a sort be written — a quantifier's binders, a grammar's non-terminals and parameters, a record field's stated sort — it accepts a Lean type or a Srt alike, through srtOf%.

def Cvc.srtOfStx : Lean.ParserDescr

srtOf% e is Srt.of e when e is a Lean type, and pure e when it is a Srt.

Equations

• Cvc.srtOfStx = Lean.ParserDescr.node `Cvc.srtOfStx 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "srtOf% ") (Lean.ParserDescr.cat `term 1024))

def Cvc.elabSrtOf : Lean.Elab.Term.TermElab

Elaborates srtOf% e by looking at what e turned out to be.

Equations

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