Sorts and their Lean descriptions

Srt is an SMT-LIB sort of the current scope, Typ a pure Lean description of one, and ToTyp the class mapping a Lean type to the Typ it denotes. The sort constructors are in Cvc.Srt.

structure Cvc.TypeGen : Type

• mk' :: (
• doc? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)
• mainId : Lean.Ident
• tParam? : Option Lean.Ident
• subId : Lean.Ident
• ofSubId : Lean.Ident
• toSubId : Lean.Ident
• idTerm : Lean.Term
• idSig : Lean.Term
• idDef : Lean.Term
• )

def Cvc.TypeGen.mk (doc? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (mainId subId : Lean.Ident) (tParam? ofSubId? toSubId? : Option Lean.Ident) : Lean.Elab.Command.CommandElabM TypeGen

Equations

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

def Cvc.TypeGen.namespaced (tg : TypeGen) {α : Type} (code : Lean.Elab.Command.CommandElabM α) : Lean.Elab.Command.CommandElabM α

Equations

• tg.namespaced code = Lean.Elab.Command.withNamespace (Lean.TSyntax.getId tg.mainId) code

def Cvc.TypeGen.elaborate (stx : Lean.Elab.Command.CommandElabM (Lean.TSyntax `command)) : Lean.Elab.Command.CommandElabM Unit

Equations

• Cvc.TypeGen.elaborate stx = do let stx ← stx Lean.Elab.Command.elabCommand stx.raw

def Cvc.TypeGen.elab0 (tg : TypeGen) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def Cvc.TypeGen.elab1 (tg : TypeGen) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def Cvc.TypeGen.elab2 (tg : TypeGen) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def Cvc.TypeGen.elab3 (tg : TypeGen) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def Cvc.cvcCustomDefKw.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.cvcCustomDefKw : Category

Equations

• Lean.Parser.Category.cvcCustomDefKw = { }

def Cvc.«cvcCustomDefKwDef0%» : Lean.ParserDescr

Equations

• Cvc.«cvcCustomDefKwDef0%» = Lean.ParserDescr.node `Cvc.«cvcCustomDefKwDef0%» 1024 (Lean.ParserDescr.symbol "def0% ")

def Cvc.«cvcCustomDefKwDef1%» : Lean.ParserDescr

Equations

• Cvc.«cvcCustomDefKwDef1%» = Lean.ParserDescr.node `Cvc.«cvcCustomDefKwDef1%» 1024 (Lean.ParserDescr.symbol "def1% ")

def Cvc.«cvcCustomDefKwDef2%» : Lean.ParserDescr

Equations

• Cvc.«cvcCustomDefKwDef2%» = Lean.ParserDescr.node `Cvc.«cvcCustomDefKwDef2%» 1024 (Lean.ParserDescr.symbol "def2% ")

def Cvc.«cvcCustomDefKwDef3%» : Lean.ParserDescr

Equations

• Cvc.«cvcCustomDefKwDef3%» = Lean.ParserDescr.node `Cvc.«cvcCustomDefKwDef3%» 1024 (Lean.ParserDescr.symbol "def3% ")

def Cvc.cvcCustomDef : Lean.ParserDescr

Equations

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

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

Equations

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

Re-exported from lean-cvc5

The enums Kind, SortKind, ProofRule and ProofRewriteRule, and the type Op, are lean-cvc5's own, re-exported so that naming one does not mean reaching into cvc5.

def Cvc.Datatype.Decl.beq [Ω] : Decl → Decl → Bool

Equality operator.

Equations

• Cvc.Datatype.Decl.beq = cvc5.DatatypeDecl.beq

def Cvc.Datatype.Decl.toString [Ω] : Decl → String

The string cvc5 prints for this value.

Equations

• Cvc.Datatype.Decl.toString = cvc5.DatatypeDecl.toString

@[instance_reducible]

instance Cvc.Datatype.Decl.instToString [Ω] : ToString Decl

Equations

• Cvc.Datatype.Decl.instToString = { toString := Cvc.Datatype.Decl.instToString._aux_1 }

def Cvc.Datatype.Decl.hash [Ω] : Decl → UInt64

cvc5's hash of this value.

Equations

• Cvc.Datatype.Decl.hash = cvc5.DatatypeDecl.hash

def Cvc.Datatype.Decl [Ω] : Type

A datatype declaration being built, which Srt.datatype turns into a sort.

Equations

• Cvc.Datatype.Decl = cvc5.DatatypeDecl

@[instance_reducible]

instance Cvc.Datatype.Decl.instHashable [Ω] : Hashable Decl

Equations

• Cvc.Datatype.Decl.instHashable = { hash := Cvc.Datatype.Decl.instHashable._aux_1 }

instance Cvc.Datatype.Decl.instNonempty [Ω] : Nonempty Decl

@[instance_reducible]

instance Cvc.Datatype.Decl.instBEq [Ω] : BEq Decl

Equations

• Cvc.Datatype.Decl.instBEq = { beq := Cvc.Datatype.Decl.instBEq._aux_1 }

def Cvc.Datatype.hash [Ω] : Datatype → UInt64

cvc5's hash of this value.

Equations

• Cvc.Datatype.hash = cvc5.Datatype.hash

@[instance_reducible]

instance Cvc.Datatype.instBEq [Ω] : BEq Datatype

Equations

• Cvc.Datatype.instBEq = { beq := Cvc.Datatype.instBEq._aux_1 }

@[instance_reducible]

instance Cvc.Datatype.instToString [Ω] : ToString Datatype

Equations

• Cvc.Datatype.instToString = { toString := Cvc.Datatype.instToString._aux_1 }

instance Cvc.Datatype.instNonempty [Ω] : Nonempty Datatype

def Cvc.Datatype.toString [Ω] : Datatype → String

The string cvc5 prints for this value.

Equations

• Cvc.Datatype.toString = cvc5.Datatype.toString

@[instance_reducible]

instance Cvc.Datatype.instHashable [Ω] : Hashable Datatype

Equations

• Cvc.Datatype.instHashable = { hash := Cvc.Datatype.instHashable._aux_1 }

def Cvc.Datatype [Ω] : Type

A declared datatype, as read back from its sort.

Equations

• Cvc.Datatype = cvc5.Datatype

def Cvc.Datatype.beq [Ω] : Datatype → Datatype → Bool

Equality operator.

Equations

• Cvc.Datatype.beq = cvc5.Datatype.beq

def Cvc.Datatype.Ctor.Decl [Ω] : Type

A constructor declaration being built, added to a Datatype.Decl.

Equations

• Cvc.Datatype.Ctor.Decl = cvc5.DatatypeConstructorDecl

def Cvc.Datatype.Ctor.Decl.toString [Ω] : Decl → String

The string cvc5 prints for this value.

Equations

• Cvc.Datatype.Ctor.Decl.toString = cvc5.DatatypeConstructorDecl.toString

def Cvc.Datatype.Ctor.Decl.beq [Ω] : Decl → Decl → Bool

Equality operator.

Equations

• Cvc.Datatype.Ctor.Decl.beq = cvc5.DatatypeConstructorDecl.beq

@[instance_reducible]

instance Cvc.Datatype.Ctor.Decl.instBEq [Ω] : BEq Decl

Equations

• Cvc.Datatype.Ctor.Decl.instBEq = { beq := Cvc.Datatype.Ctor.Decl.instBEq._aux_1 }

instance Cvc.Datatype.Ctor.Decl.instNonempty [Ω] : Nonempty Decl

def Cvc.Datatype.Ctor.Decl.hash [Ω] : Decl → UInt64

cvc5's hash of this value.

Equations

• Cvc.Datatype.Ctor.Decl.hash = cvc5.DatatypeConstructorDecl.hash

@[instance_reducible]

instance Cvc.Datatype.Ctor.Decl.instToString [Ω] : ToString Decl

Equations

• Cvc.Datatype.Ctor.Decl.instToString = { toString := Cvc.Datatype.Ctor.Decl.instToString._aux_1 }

@[instance_reducible]

instance Cvc.Datatype.Ctor.Decl.instHashable [Ω] : Hashable Decl

Equations

• Cvc.Datatype.Ctor.Decl.instHashable = { hash := Cvc.Datatype.Ctor.Decl.instHashable._aux_1 }

def Cvc.Datatype.Ctor.toString [Ω] : Ctor → String

The string cvc5 prints for this value.

Equations

• Cvc.Datatype.Ctor.toString = cvc5.DatatypeConstructor.toString

def Cvc.Datatype.Ctor.beq [Ω] : Ctor → Ctor → Bool

Equality operator.

Equations

• Cvc.Datatype.Ctor.beq = cvc5.DatatypeConstructor.beq

def Cvc.Datatype.Ctor [Ω] : Type

A constructor of a declared datatype.

Equations

• Cvc.Datatype.Ctor = cvc5.DatatypeConstructor

def Cvc.Datatype.Ctor.hash [Ω] : Ctor → UInt64

cvc5's hash of this value.

Equations

• Cvc.Datatype.Ctor.hash = cvc5.DatatypeConstructor.hash

@[instance_reducible]

instance Cvc.Datatype.Ctor.instToString [Ω] : ToString Ctor

Equations

• Cvc.Datatype.Ctor.instToString = { toString := Cvc.Datatype.Ctor.instToString._aux_1 }

instance Cvc.Datatype.Ctor.instNonempty [Ω] : Nonempty Ctor

@[instance_reducible]

instance Cvc.Datatype.Ctor.instHashable [Ω] : Hashable Ctor

Equations

• Cvc.Datatype.Ctor.instHashable = { hash := Cvc.Datatype.Ctor.instHashable._aux_1 }

@[instance_reducible]

instance Cvc.Datatype.Ctor.instBEq [Ω] : BEq Ctor

Equations

• Cvc.Datatype.Ctor.instBEq = { beq := Cvc.Datatype.Ctor.instBEq._aux_1 }

def Cvc.Datatype.Selector [Ω] : Type

A field selector of a datatype constructor.

Equations

• Cvc.Datatype.Selector = cvc5.DatatypeSelector

@[instance_reducible]

instance Cvc.Datatype.Selector.instToString [Ω] : ToString Selector

Equations

• Cvc.Datatype.Selector.instToString = { toString := Cvc.Datatype.Selector.instToString._aux_1 }

@[instance_reducible]

instance Cvc.Datatype.Selector.instBEq [Ω] : BEq Selector

Equations

• Cvc.Datatype.Selector.instBEq = { beq := Cvc.Datatype.Selector.instBEq._aux_1 }

instance Cvc.Datatype.Selector.instNonempty [Ω] : Nonempty Selector

@[instance_reducible]

instance Cvc.Datatype.Selector.instHashable [Ω] : Hashable Selector

Equations

• Cvc.Datatype.Selector.instHashable = { hash := Cvc.Datatype.Selector.instHashable._aux_1 }

def Cvc.Datatype.Selector.toString [Ω] : Selector → String

The string cvc5 prints for this value.

Equations

• Cvc.Datatype.Selector.toString = cvc5.DatatypeSelector.toString

def Cvc.Datatype.Selector.hash [Ω] : Selector → UInt64

cvc5's hash of this value.

Equations

• Cvc.Datatype.Selector.hash = cvc5.DatatypeSelector.hash

def Cvc.Datatype.Selector.beq [Ω] : Selector → Selector → Bool

Equality operator.

Equations

• Cvc.Datatype.Selector.beq = cvc5.DatatypeSelector.beq

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

Less than or equal comparison.

Equations

• Cvc.Srt.ble = cvc5.Sort.ble

def Cvc.Srt [Ω] : Type

An SMT-LIB sort of the current scope.

Built with Srt.int, Srt.set and the other constructors, or from a Lean type with Srt.of.

Equations

• Cvc.Srt = cvc5.Sort

@[instance_reducible]

instance Cvc.Srt.instDecidableLT [Ω] : DecidableLT Srt

Equations

• Cvc.Srt.instDecidableLT = Cvc.Srt.instDecidableLT._aux_1

@[instance_reducible]

instance Cvc.Srt.instOrd [Ω] : Ord Srt

Equations

• Cvc.Srt.instOrd = { compare := Cvc.Srt.instOrd._aux_1 }

@[instance_reducible]

instance Cvc.Srt.instDecidableLE [Ω] : DecidableLE Srt

Equations

• Cvc.Srt.instDecidableLE = Cvc.Srt.instDecidableLE._aux_1

@[instance_reducible]

instance Cvc.Srt.instToString [Ω] : ToString Srt

Equations

• Cvc.Srt.instToString = { toString := Cvc.Srt.instToString._aux_1 }

instance Cvc.Srt.instNonempty [Ω] : Nonempty Srt

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

Greater than or equal comparison.

Equations

• Cvc.Srt.bge = cvc5.Sort.bge

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

Comparison for structural equality.

Equations

• Cvc.Srt.beq = cvc5.Sort.beq

@[instance_reducible]

instance Cvc.Srt.instLE [Ω] : LE Srt

Equations

• Cvc.Srt.instLE = { le := Cvc.Srt.instLE._aux_1 }

def Cvc.Srt.compare [Ω] : Srt → Srt → Ordering

Comparison of two sorts.

Equations

• Cvc.Srt.compare = cvc5.Sort.compare

def Cvc.Srt.hash [Ω] : Srt → UInt64

cvc5's hash of this value.

Equations

• Cvc.Srt.hash = cvc5.Sort.hash

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

Greater than comparison.

Equations

• Cvc.Srt.bgt = cvc5.Sort.bgt

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

Less than comparison.

Equations

• Cvc.Srt.blt = cvc5.Sort.blt

def Cvc.Srt.toString [Ω] : Srt → String

The string cvc5 prints for this value.

Equations

• Cvc.Srt.toString = cvc5.Sort.toString

@[instance_reducible]

instance Cvc.Srt.instBEq [Ω] : BEq Srt

Equations

• Cvc.Srt.instBEq = { beq := Cvc.Srt.instBEq._aux_1 }

@[instance_reducible]

instance Cvc.Srt.instHashable [Ω] : Hashable Srt

Equations

• Cvc.Srt.instHashable = { hash := Cvc.Srt.instHashable._aux_1 }

@[instance_reducible]

instance Cvc.Srt.instLT [Ω] : LT Srt

Equations

• Cvc.Srt.instLT = { lt := Cvc.Srt.instLT._aux_1 }

inductive Cvc.Srt.Abstract : Type

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

• bitVec : Abstract
• float : Abstract
• finiteField : Abstract
• function : Abstract

@[instance_reducible]

instance Cvc.Srt.instInhabitedAbstract : Inhabited Abstract

Equations

• Cvc.Srt.instInhabitedAbstract = { default := Cvc.Srt.instInhabitedAbstract.default }

@[instance_reducible]

instance Cvc.Srt.instDecidableEqAbstract : DecidableEq Abstract

Equations

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

@[instance_reducible]

instance Cvc.Srt.instBEqAbstract : BEq Abstract

Equations

• Cvc.Srt.instBEqAbstract = { beq := Cvc.Srt.instBEqAbstract.beq }

def Cvc.Srt.instBEqAbstract.beq : Abstract → Abstract → Bool

Equations

• Cvc.Srt.instBEqAbstract.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Cvc.Srt.instOrdAbstract : Ord Abstract

Equations

• Cvc.Srt.instOrdAbstract = { compare := Cvc.Srt.instOrdAbstract.ord }

def Cvc.Srt.instOrdAbstract.ord : Abstract → Abstract → Ordering

Equations

• Cvc.Srt.instOrdAbstract.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

def Cvc.Srt.instHashableAbstract.hash : Abstract → UInt64

Equations

• Cvc.Srt.instHashableAbstract.hash Cvc.Srt.Abstract.bitVec = 0
• Cvc.Srt.instHashableAbstract.hash Cvc.Srt.Abstract.float = 1
• Cvc.Srt.instHashableAbstract.hash Cvc.Srt.Abstract.finiteField = 2
• Cvc.Srt.instHashableAbstract.hash Cvc.Srt.Abstract.function = 3

@[instance_reducible]

instance Cvc.Srt.instHashableAbstract : Hashable Abstract

Equations

• Cvc.Srt.instHashableAbstract = { hash := Cvc.Srt.instHashableAbstract.hash }

def Cvc.Srt.instReprAbstract.repr : Abstract → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cvc.Srt.instReprAbstract : Repr Abstract

Equations

• Cvc.Srt.instReprAbstract = { reprPrec := Cvc.Srt.instReprAbstract.repr }

def Cvc.Srt.Abstract.toString (a : Abstract) : String

Equations

• Cvc.Srt.Abstract.bitVec.toString = "BitVec _"
• Cvc.Srt.Abstract.float.toString = "Float _ _"
• Cvc.Srt.Abstract.finiteField.toString = "FiniteField _"
• Cvc.Srt.Abstract.function.toString = "_ → _"

@[instance_reducible]

instance Cvc.Srt.Abstract.instToString : ToString Abstract

Equations

• Cvc.Srt.Abstract.instToString = { toString := Cvc.Srt.Abstract.toString }

def Cvc.Srt.Abstract.toKind (a : Abstract) : SortKind

Equations

• Cvc.Srt.Abstract.bitVec.toKind = cvc5.SortKind.BITVECTOR_SORT
• Cvc.Srt.Abstract.float.toKind = cvc5.SortKind.FLOATINGPOINT_SORT
• Cvc.Srt.Abstract.finiteField.toKind = cvc5.SortKind.FINITE_FIELD_SORT
• Cvc.Srt.Abstract.function.toKind = cvc5.SortKind.FUNCTION_SORT

@[instance_reducible]

instance Cvc.Srt.Abstract.instOrd : Ord Abstract

Equations

• Cvc.Srt.Abstract.instOrd = { compare := fun (a1 a2 : Cvc.Srt.Abstract) => compare a1.ctorIdx a2.ctorIdx }

def Cvc.Srt.Abstract.ble (a1 a2 : Abstract) : Bool

Equations

• a1.ble a2 = decide (a1.ctorIdx ≤ a2.ctorIdx)

def Cvc.Srt.Abstract.blt (a1 a2 : Abstract) : Bool

Equations

• a1.blt a2 = decide (a1.ctorIdx < a2.ctorIdx)

@[instance_reducible]

instance Cvc.Srt.Abstract.instLE : LE Abstract

Equations

• Cvc.Srt.Abstract.instLE = { le := fun (x1 x2 : Cvc.Srt.Abstract) => x1.ble x2 = true }

@[instance_reducible]

instance Cvc.Srt.Abstract.instDecidableLE : DecidableLE Abstract

Equations

• a1.instDecidableLE a2 = if h : a1.ble a2 = true then isTrue h else isFalse h

@[instance_reducible]

instance Cvc.Srt.Abstract.instLT : LT Abstract

Equations

• Cvc.Srt.Abstract.instLT = { lt := fun (x1 x2 : Cvc.Srt.Abstract) => x1.blt x2 = true }

@[instance_reducible]

instance Cvc.Srt.Abstract.instDecidableLT : DecidableLT Abstract

Equations

• a1.instDecidableLT a2 = if h : a1.blt a2 = true then isTrue h else isFalse h

@[reducible, inline]

abbrev Cvc.Srts [Ω] : Type

An array of Srts.

Equations

• Cvc.Srts = Array Cvc.Srt

Sort descriptions

Typ describes a sort Lean-side, and Typ? adds the sorts cvc5 calls abstract: the fully abstract ?, and ?BITVECTOR_TYPE, ?FLOATINGPOINT_TYPE, ?FINITE_FIELD_TYPE and ?->. cvc5 accepts an abstract sort only as a set, bag or sequence element, as an array's index or element, and as a function's codomain. Those positions take a Typ? and every other takes a Typ, so no Typ describes a sort cvc5 would reject.

inductive Cvc.Typ : Type

A sort, described Lean-side; never an abstract sort.

• bool : Typ
• int : Typ
• real : Typ
• string : Typ
• regex : Typ
• roundingMode : Typ
• bitVec (size : Nat) : Typ
• float (exp sig : Nat) : Typ
• finiteField (size : Nat) : Typ
• arrayTo (idx elm : Typ?) : Typ
• bag (elm : Typ?) : Typ
• set (elm : Typ?) : Typ
• seq (elm : Typ?) : Typ
• nullable (elm : Typ) : Typ

  cvc5's Nullable, denoted Lean-side by Option.

• prod (args : List Typ) : Typ

  A tuple, of the given components.

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

  A record, of named fields.

  The order is part of the sort: {a : Int, b : Bool} and {b : Bool, a : Int} are different.

• datatype (name : String) : Typ

  A datatype, by the name it was declared under.

  Typ.toSrt fails unless a datatype of that name has been declared in the current scope, with Srt.datatype, Srt.datatypes or Solver.declareDatatype.

• function (dom : Typ) (cod : Typ?) : Typ

  A function sort, its codomain possibly abstract.

• uninterpreted (name : String) : Typ

  An uninterpreted sort, by name; like datatype, it must be declared (Srt.uninterpreted).

inductive Cvc.Typ? : Type

A Typ, or one of the sorts cvc5 calls abstract, for the positions that accept one.

• typ (t : Typ) : Typ?

  An ordinary, first-class sort.

• any : Typ?

  cvc5's fully abstract sort ?.

• abstract (a : Srt.Abstract) : Typ?

  An abstract sort of a known kind, ?BITVECTOR_TYPE and friends.

@[instance_reducible]

def Cvc.instOrdProd_cvc {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] : Ord (α × β)

Equations

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

@[instance_reducible]

instance Cvc.instOrdTyp : Ord Typ

Equations

• Cvc.instOrdTyp = { compare := Cvc.instOrdTyp.ord_1 }

partial def Cvc.instOrdTyp.ord_1 : Typ → Typ → Ordering

partial def Cvc.instOrdTyp?.ord_1 : Typ → Typ → Ordering

partial def Cvc.instOrdTyp?.ord_2 : Typ? → Typ? → Ordering

@[instance_reducible]

instance Cvc.instOrdTyp? : Ord Typ?

Equations

• Cvc.instOrdTyp? = { compare := Cvc.instOrdTyp?.ord_2 }

partial def Cvc.instOrdTyp.ord_2 : Typ? → Typ? → Ordering

partial def Cvc.instHashableTyp?.hash_2 : Typ? → UInt64

partial def Cvc.instHashableTyp.hash_1 : Typ → UInt64

partial def Cvc.instHashableTyp.hash_2 : Typ? → UInt64

@[instance_reducible]

instance Cvc.instHashableTyp : Hashable Typ

Equations

• Cvc.instHashableTyp = { hash := Cvc.instHashableTyp.hash_1 }

partial def Cvc.instHashableTyp?.hash_1 : Typ → UInt64

@[instance_reducible]

instance Cvc.instHashableTyp? : Hashable Typ?

Equations

• Cvc.instHashableTyp? = { hash := Cvc.instHashableTyp?.hash_2 }

@[instance_reducible]

instance Cvc.instCoeTypTyp? : Coe Typ Typ?

Every Typ is a Typ?, so the wrapping is implicit.

Equations

• Cvc.instCoeTypTyp? = { coe := Cvc.Typ?.typ }

Typ's constructors, mirrored

Dot notation resolves against the expected type, so .set .int would look for Typ?.int and fail. These restore it, and @[match_pattern] makes them usable in patterns as well as in terms.

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.bool : Typ?

Equations

• Cvc.Typ?.bool = Cvc.Typ?.typ Cvc.Typ.bool

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.int : Typ?

Equations

• Cvc.Typ?.int = Cvc.Typ?.typ Cvc.Typ.int

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.real : Typ?

Equations

• Cvc.Typ?.real = Cvc.Typ?.typ Cvc.Typ.real

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.string : Typ?

Equations

• Cvc.Typ?.string = Cvc.Typ?.typ Cvc.Typ.string

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.regex : Typ?

Equations

• Cvc.Typ?.regex = Cvc.Typ?.typ Cvc.Typ.regex

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.roundingMode : Typ?

Equations

• Cvc.Typ?.roundingMode = Cvc.Typ?.typ Cvc.Typ.roundingMode

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.bitVec (size : Nat) : Typ?

Equations

• Cvc.Typ?.bitVec size = Cvc.Typ?.typ (Cvc.Typ.bitVec size)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.float (exp sig : Nat) : Typ?

Equations

• Cvc.Typ?.float exp sig = Cvc.Typ?.typ (Cvc.Typ.float exp sig)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.finiteField (size : Nat) : Typ?

Equations

• Cvc.Typ?.finiteField size = Cvc.Typ?.typ (Cvc.Typ.finiteField size)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.arrayTo (idx elm : Typ?) : Typ?

Equations

• idx.arrayTo elm = Cvc.Typ?.typ (Cvc.Typ.arrayTo idx elm)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.bag (elm : Typ?) : Typ?

Equations

• elm.bag = Cvc.Typ?.typ (Cvc.Typ.bag elm)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.set (elm : Typ?) : Typ?

Equations

• elm.set = Cvc.Typ?.typ (Cvc.Typ.set elm)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.seq (elm : Typ?) : Typ?

Equations

• elm.seq = Cvc.Typ?.typ (Cvc.Typ.seq elm)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.nullable (elm : Typ) : Typ?

Equations

• Cvc.Typ?.nullable elm = Cvc.Typ?.typ elm.nullable

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.prod (args : List Typ) : Typ?

Equations

• Cvc.Typ?.prod args = Cvc.Typ?.typ (Cvc.Typ.prod args)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.record (fields : List (String × Typ)) : Typ?

Equations

• Cvc.Typ?.record fields = Cvc.Typ?.typ (Cvc.Typ.record fields)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.datatype (name : String) : Typ?

Equations

• Cvc.Typ?.datatype name = Cvc.Typ?.typ (Cvc.Typ.datatype name)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.function (dom : Typ) (cod : Typ?) : Typ?

Equations

• Cvc.Typ?.function dom cod = Cvc.Typ?.typ (dom.function cod)

@[reducible, match_pattern, inline]

abbrev Cvc.Typ?.uninterpreted (name : String) : Typ?

Equations

• Cvc.Typ?.uninterpreted name = Cvc.Typ?.typ (Cvc.Typ.uninterpreted name)

def Cvc.Typ.beq : Typ → Typ → Bool

Structural equality.

Equations

• Cvc.Typ.bool.beq Cvc.Typ.bool = true
• Cvc.Typ.int.beq Cvc.Typ.int = true
• Cvc.Typ.real.beq Cvc.Typ.real = true
• Cvc.Typ.string.beq Cvc.Typ.string = true
• Cvc.Typ.regex.beq Cvc.Typ.regex = true
• Cvc.Typ.roundingMode.beq Cvc.Typ.roundingMode = true
• (Cvc.Typ.bitVec s₁).beq (Cvc.Typ.bitVec s₂) = (s₁ == s₂)
• (Cvc.Typ.float e₁ s₁).beq (Cvc.Typ.float e₂ s₂) = (e₁ == e₂ && s₁ == s₂)
• (Cvc.Typ.finiteField s₁).beq (Cvc.Typ.finiteField s₂) = (s₁ == s₂)
• (Cvc.Typ.arrayTo i₁ e₁).beq (Cvc.Typ.arrayTo i₂ e₂) = (i₁.beq i₂ && e₁.beq e₂)
• (Cvc.Typ.bag e₁).beq (Cvc.Typ.bag e₂) = e₁.beq e₂
• (Cvc.Typ.set e₁).beq (Cvc.Typ.set e₂) = e₁.beq e₂
• (Cvc.Typ.seq e₁).beq (Cvc.Typ.seq e₂) = e₁.beq e₂
• e₁.nullable.beq e₂.nullable = e₁.beq e₂
• (Cvc.Typ.prod as₁).beq (Cvc.Typ.prod as₂) = Cvc.Typ.beqList as₁ as₂
• (Cvc.Typ.record fs₁).beq (Cvc.Typ.record fs₂) = Cvc.Typ.beqFields fs₁ fs₂
• (Cvc.Typ.datatype n₁).beq (Cvc.Typ.datatype n₂) = (n₁ == n₂)
• (d₁.function c₁).beq (d₂.function c₂) = (d₁.beq d₂ && c₁.beq c₂)
• (Cvc.Typ.uninterpreted name₁).beq (Cvc.Typ.uninterpreted name₂) = (name₁ == name₂)
• x✝¹.beq x✝ = false

def Cvc.Typ.beqList : List Typ → List Typ → Bool

Structural equality.

Equations

• Cvc.Typ.beqList [] [] = true
• Cvc.Typ.beqList (hd₁ :: tl₁) (hd₂ :: tl₂) = (hd₁.beq hd₂ && Cvc.Typ.beqList tl₁ tl₂)
• Cvc.Typ.beqList x✝¹ x✝ = false

def Cvc.Typ.beqFields : List (String × Typ) → List (String × Typ) → Bool

Structural equality.

Equations

• Cvc.Typ.beqFields [] [] = true
• Cvc.Typ.beqFields ((n₁, t₁) :: r₁) ((n₂, t₂) :: r₂) = (n₁ == n₂ && t₁.beq t₂ && Cvc.Typ.beqFields r₁ r₂)
• Cvc.Typ.beqFields x✝¹ x✝ = false

def Cvc.Typ?.beq : Typ? → Typ? → Bool

Structural equality.

Equations

• (Cvc.Typ?.typ t₁).beq (Cvc.Typ?.typ t₂) = t₁.beq t₂
• Cvc.Typ?.any.beq Cvc.Typ?.any = true
• (Cvc.Typ?.abstract a₁).beq (Cvc.Typ?.abstract a₂) = decide (a₁ = a₂)
• x✝¹.beq x✝ = false

theorem Cvc.Typ.beq_refl (t : Typ) : t.beq t = true

Cvc.Typ.beq is reflexive.

theorem Cvc.Typ.beqList_refl (ts : List Typ) : Typ.beqList ts ts = true

Cvc.Typ.beq is reflexive.

theorem Cvc.Typ.beqFields_refl (fs : List (String × Typ)) : Typ.beqFields fs fs = true

Cvc.Typ.beq is reflexive.

theorem Cvc.Typ?.beq_refl (t : Typ?) : t.beq t = true

Cvc.Typ.beq is reflexive.

theorem Cvc.Typ.eq_of_beq (t₁ t₂ : Typ) : t₁.beq t₂ = true → t₁ = t₂

Cvc.Typ.beq holds only of equals.

theorem Cvc.Typ.eq_of_beqList (ts₁ ts₂ : List Typ) : Typ.beqList ts₁ ts₂ = true → ts₁ = ts₂

Cvc.Typ.beq holds only of equals.

theorem Cvc.Typ.eq_of_beqFields (fs₁ fs₂ : List (String × Typ)) : Typ.beqFields fs₁ fs₂ = true → fs₁ = fs₂

Cvc.Typ.beq holds only of equals.

theorem Cvc.Typ?.eq_of_beq (t₁ t₂ : Typ?) : t₁.beq t₂ = true → t₁ = t₂

Cvc.Typ.beq holds only of equals.

@[instance_reducible]

instance Cvc.Typ.instDecidableEq : DecidableEq Typ

Equations

• t₁.instDecidableEq t₂ = decidable_of_iff (t₁.beq t₂ = true) ⋯

@[instance_reducible]

instance Cvc.Typ?.instDecidableEq : DecidableEq Typ?

Equations

• t₁.instDecidableEq t₂ = decidable_of_iff (t₁.beq t₂ = true) ⋯

def Cvc.Typ.toString (t : Typ) (paren : Bool := false) : String

String representation.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Typ.bool.toString paren = "Bool"
• Cvc.Typ.int.toString paren = "Int"
• Cvc.Typ.real.toString paren = "Real"
• Cvc.Typ.string.toString paren = "String"
• Cvc.Typ.regex.toString paren = "Regex"
• Cvc.Typ.roundingMode.toString paren = "RoundingMode"
• (Cvc.Typ.bitVec size).toString paren = (fun (s : String) => if paren = true then toString "(" ++ toString s ++ toString ")" else s) (toString "BitVec " ++ toString size)
• (Cvc.Typ.finiteField size).toString paren = (fun (s : String) => if paren = true then toString "(" ++ toString s ++ toString ")" else s) (toString "FiniteField " ++ toString size)
• (Cvc.Typ.bag elm).toString paren = (fun (s : String) => if paren = true then toString "(" ++ toString s ++ toString ")" else s) (toString "Bag " ++ toString (elm.toString true))
• (Cvc.Typ.set elm).toString paren = (fun (s : String) => if paren = true then toString "(" ++ toString s ++ toString ")" else s) (toString "Set " ++ toString (elm.toString true))
• (Cvc.Typ.seq elm).toString paren = (fun (s : String) => if paren = true then toString "(" ++ toString s ++ toString ")" else s) (toString "Seq " ++ toString (elm.toString true))
• elm.nullable.toString paren = (fun (s : String) => if paren = true then toString "(" ++ toString s ++ toString ")" else s) (toString "Option " ++ toString (elm.toString true))
• (Cvc.Typ.prod []).toString paren = "Unit"
• (Cvc.Typ.prod [α]).toString paren = toString "(× " ++ toString α.toString ++ toString ")"
• (Cvc.Typ.prod args).toString paren = (fun (s : String) => if paren = true then toString "(" ++ toString s ++ toString ")" else s) (Cvc.Typ.tupleArgsFold args "")
• (Cvc.Typ.datatype name).toString paren = name

def Cvc.Typ?.toString (t : Typ?) (paren : Bool := false) : String

String representation.

Equations

• (Cvc.Typ?.typ a).toString paren = a.toString paren
• Cvc.Typ?.any.toString paren = "?"
• (Cvc.Typ?.abstract a).toString paren = if paren = true then toString "(Abstract " ++ toString a ++ toString ")" else toString "Abstract " ++ toString a

def Cvc.Typ.fieldsFold (fields : List (String × Typ)) (acc : String) : String

Renders a record's fields, for Typ.toString.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Typ.fieldsFold [] x✝ = x✝

def Cvc.Typ.tupleArgsFold (args : List Typ) (acc : String) : String

Renders a tuple's components, for Typ.toString.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Typ.tupleArgsFold [] "" = "Unit"
• Cvc.Typ.tupleArgsFold [ty] "" = toString "(× " ++ toString ty.toString ++ toString ")"
• Cvc.Typ.tupleArgsFold [] x✝ = x✝

@[instance_reducible]

instance Cvc.instToStringTyp : ToString Typ

Equations

• Cvc.instToStringTyp = { toString := fun (x : Cvc.Typ) => x.toString }

@[instance_reducible]

instance Cvc.instToStringTyp? : ToString Typ?

Equations

• Cvc.instToStringTyp? = { toString := fun (x : Cvc.Typ?) => x.toString }

class Cvc.ToTyp (α : Type) : Type

The sort a Lean type denotes, which lets it index terms.

For a declared datatype, name it and declare it in the scope before use: instance : ToTyp Pair := ⟨.datatype "Pair"⟩.

• typ : Typ

  Typ associated to a type through ToTyp.