def Cvc.Symbol.At.mkName (name : String) (k : Nat) : String

Generates the unrolled version of a symbol's name.

Argument name should be the Symbol.name of a not-unrolled symbol.

Equations

• Cvc.Symbol.At.mkName name k = toString "" ++ toString name ++ toString "_unrolled_at_" ++ toString k ++ toString ""

structure Cvc.Symbol.At (k : Nat) (β α : Type) : Type

A symbol unrolled at some depth k, whatever depth means.

• getSymbol : Symbol β α

  Private conversion to syms, not reason to use this directly currently.

@[reducible, inline]

abbrev Cvc.Symbol.IdentAt (k : Nat) (α : Type) : Type

Type alias for a Symbol.Ident at some depth.

Equations

• Cvc.Symbol.IdentAt k α = Cvc.Symbol.At k String α

@[reducible, inline]

abbrev Cvc.Symbol.TermAt (k : semiOutParam Nat) (α : Type) : Type

Type alias for a Symbol.Term at some depth.

Equations

• Cvc.Symbol.TermAt k α = Cvc.Symbol.At k (Cvc.Term α) α

@[reducible, inline]

abbrev Cvc.Symbol.ValueAt (k : Nat) (α : Type) : Type

Type alias for a Symbol.Val at some depth.

Equations

• Cvc.Symbol.ValueAt k α = Cvc.Symbol.At k (Cvc.Value α) α

instance Cvc.Symbol.instCoeDepTermAtTerm {k : Nat} {α : Type} {term : TermAt k α} : CoeDep (TermAt k α) term (Term α)

Equations

• Cvc.Symbol.instCoeDepTermAtTerm = { coe := term.getSymbol.get }

@[defaultInstance 1000]

instance Cvc.Symbol.At.instGetter {k : Nat} {β α : Type} : Getter (Symbol.At k β α) β

Equations

• Cvc.Symbol.At.instGetter = { getInner := fun (s : Cvc.Symbol.At k β α) => s.getSymbol.get }

instance Cvc.Symbol.At.instToString {β : Type} {k : Nat} {α : Type} [ToString β] : ToString (Symbol.At k β α)

Equations

• Cvc.Symbol.At.instToString = { toString := fun (s : Cvc.Symbol.At k β α) => toString s.getSymbol.get }

def Cvc.Symbol.At.name {k : Nat} {β α : Type} (sym : Symbol.At k β α) : String

Equations

• sym.name = Cvc.Symbol.At.mkName sym.getSymbol.name k

def Cvc.Symbol.At.mapM {m : Type → Type u_1} {k : Nat} {β α : Type} [Monad m] (sym : Symbol.At k β α) {γ : Type} (f : β → m γ) : m (Symbol.At k γ α)

Equations

• sym.mapM f = Cvc.Symbol.At.mapSymbolM✝ sym fun (s : Cvc.Symbol β α) => s.mapM f

def Cvc.Symbol.At.map {k : Nat} {β α γ : Type} (sym : Symbol.At k β α) (f : β → γ) : Symbol.At k γ α

Equations

• sym.map f = sym.mapM f

def Cvc.Symbol.IdentAt.ofIdent {α : Type} (ident : Symbol.Ident α) (k : Nat := 0) : IdentAt k α

Equations

• Cvc.Symbol.IdentAt.ofIdent ident k = { getSymbol := { name := ident.name, get := Cvc.Symbol.At.mkName ident.name k } }

def Cvc.Symbol.IdentAt.getIdent {α : Type} {k : Nat} (ident : IdentAt k α) : Symbol.Ident α

Equations

• ident.getIdent = Cvc.Symbol.Ident.mk (Cvc.Symbol.At.name ident)

def Cvc.Symbol.IdentAt.unroll {α : Type} {k : Nat} (ident : IdentAt k α) (k' : Nat := k.succ) : IdentAt k' α

Equations

• ident.unroll k' = Cvc.Symbol.IdentAt.ofIdent ident.getIdent k'

def Cvc.Symbol.IdentAt.next {α : Type} {k : Nat} (ident : IdentAt k α) : IdentAt k.succ α

Equations

• ident.next = ident.unroll

def Cvc.Symbol.IdentAt.declare {α : Type} {k : Nat} [IsSrt α] (ident : IdentAt k α) : Smt (TermAt k α)

Equations

• ident.declare = Cvc.Symbol.At.mapSymbolM✝ ident fun (x : Cvc.Symbol String α) => x.declare

def Cvc.Symbol.Ident.unroll {α : Type} (ident : Symbol.Ident α) (k : Nat := 0) : IdentAt k α

Equations

• ident.unroll k = Cvc.Symbol.IdentAt.ofIdent ident k

def Cvc.Symbol.Ident.declareAt {α : Type} [IsSrt α] (ident : Symbol.Ident α) (k : Nat := 0) : Smt (TermAt k α)

Equations

• ident.declareAt k = (ident.unroll k).declare

def Cvc.Symbol.TermAt.getValue {α : Type} {k : Nat} [IsSrt α] (term : TermAt k α) : Smt.Sat (ValueAt k α)

Equations

• term.getValue = Cvc.Symbol.At.mapSymbolM✝ term Cvc.Symbol.getValue

@[reducible, inline]

abbrev Cvc.Symbols.IdentsAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• Cvc.Symbols.IdentsAt k = Struct fun (x : Type) [Cvc.IsSrt x] => Cvc.Symbol.IdentAt k x

@[reducible, inline]

abbrev Cvc.Symbols.TermsAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• Cvc.Symbols.TermsAt k = Struct fun (x : Type) [Cvc.IsSrt x] => Cvc.Symbol.TermAt k x

@[reducible, inline]

abbrev Cvc.Symbols.ModelAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• Cvc.Symbols.ModelAt k = Struct fun (x : Type) [Cvc.IsSrt x] => Cvc.Symbol.ValueAt k x

@[reducible, inline]

abbrev Cvc.Symbols.ValuesAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• Cvc.Symbols.ValuesAt k = Cvc.Symbols.ModelAt k

@[reducible, inline]

abbrev Cvc.Symbols.FunMAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (m : Type → Type u_1) (k : Nat) (α : Type) : Type u_1

Equations

• Cvc.Symbols.FunMAt m k α = (Cvc.Symbols.TermsAt k → Cvc.Term.BuildT m (Cvc.Term α))

@[reducible, inline]

abbrev Cvc.Symbols.FunctionMAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (m : Type → Type u_1) (k : Nat) (α : Type) : Type u_1

Equations

• @Cvc.Symbols.FunctionMAt = @Cvc.Symbols.FunMAt

@[reducible, inline]

abbrev Cvc.Symbols.FunAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) (α : Type) : Type

Equations

• Cvc.Symbols.FunAt k α = Cvc.Symbols.FunMAt Id k α

@[reducible, inline]

abbrev Cvc.Symbols.FunctionAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) (α : Type) : Type

Equations

• @Cvc.Symbols.FunctionAt = @Cvc.Symbols.FunAt

@[reducible, inline]

abbrev Cvc.Symbols.PredAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• Cvc.Symbols.PredAt k = Cvc.Symbols.FunAt k Bool

@[reducible, inline]

abbrev Cvc.Symbols.PredicateAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• @Cvc.Symbols.PredicateAt = @Cvc.Symbols.PredAt

@[reducible, inline]

abbrev Cvc.Symbols.StatePred {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.StatePred = ({k : Nat} → Cvc.Symbols.PredAt k)

@[reducible, inline]

abbrev Cvc.Symbols.StatePredicate {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.StatePredicate = Cvc.Symbols.StatePred

@[reducible, inline]

abbrev Cvc.Symbols.RelAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• Cvc.Symbols.RelAt k = (Cvc.Symbols.TermsAt k → Cvc.Symbols.PredAt k.succ)

@[reducible, inline]

abbrev Cvc.Symbols.RelationAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• @Cvc.Symbols.RelationAt = @Cvc.Symbols.RelAt

@[reducible, inline]

abbrev Cvc.Symbols.StateRel {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.StateRel = ({k : Nat} → Cvc.Symbols.RelAt k)

@[reducible, inline]

abbrev Cvc.Symbols.StateRelation {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.StateRelation = Cvc.Symbols.StateRel

@[reducible, inline]

abbrev Cvc.Symbols.InvRelAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• Cvc.Symbols.InvRelAt k = (Cvc.Symbols.TermsAt k.succ → Cvc.Symbols.PredAt k)

@[reducible, inline]

abbrev Cvc.Symbols.InvRelationAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (k : Nat) : Type

Equations

• @Cvc.Symbols.InvRelationAt = @Cvc.Symbols.InvRelAt

@[reducible, inline]

abbrev Cvc.Symbols.StateInvRel {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.StateInvRel = ({k : Nat} → Cvc.Symbols.InvRelAt k)

@[reducible, inline]

abbrev Cvc.Symbols.StateInvRelation {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.StateInvRelation = Cvc.Symbols.StateInvRel

@[reducible, inline]

abbrev Cvc.Symbols.NamedPreds {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.NamedPreds = Cvc.RBMap String Cvc.Symbols.StatePred

@[reducible, inline]

abbrev Cvc.Symbols.NamedPredicates {Struct : Symbols.Repr} [Syms : Symbols Struct] : Type

Equations

• Cvc.Symbols.NamedPredicates = Cvc.Symbols.NamedPreds

def Cvc.Symbols.IdentsAt.mapM {Struct : Symbols.Repr} [Syms : Symbols Struct] {m : Type → Type} {k : Nat} {R : Symbol.Repr} [Monad m] (syms : IdentsAt k) (f : {α : Type} → [inst : IsSrt α] → Symbol.IdentAt k α → m (R α)) : m (Struct R)

Equations

• syms.mapM f = Cvc.Symbols.mapM syms fun {α : Type} [Cvc.IsSrt α] => f

def Cvc.Symbols.IdentsAt.map {Struct : Symbols.Repr} [Syms : Symbols Struct] {k : Nat} {R : Symbol.Repr} (syms : IdentsAt k) (f : {α : Type} → [inst : IsSrt α] → Symbol.IdentAt k α → R α) : Struct R

Equations

• syms.map f = syms.mapM fun {α : Type} [Cvc.IsSrt α] => f

def Cvc.Symbols.IdentsAt.unroll {Struct : Symbols.Repr} [Syms : Symbols Struct] (syms : Idents) (k : Nat := 0) : IdentsAt k

Equations

• Cvc.Symbols.unroll syms k = Cvc.Symbols.map syms fun {α : Type} [Cvc.IsSrt α] (x : Cvc.Symbol.Ident α) => x.unroll k

def Cvc.Symbols.IdentsAt.next {Struct : Symbols.Repr} [Syms : Symbols Struct] {k : Nat} (syms : IdentsAt k) : IdentsAt k.succ

Equations

• syms.next = syms.map fun {α : Type} [Cvc.IsSrt α] => Cvc.Symbol.IdentAt.next

def Cvc.Symbols.IdentsAt.declareAt {Struct : Symbols.Repr} [Syms : Symbols Struct] (syms : Idents) (k : Nat) : Smt (TermsAt k)

Equations

• Cvc.Symbols.declareAt syms k = Cvc.Symbols.IdentsAt.declare✝ (Cvc.Symbols.unroll syms k)

def Cvc.Symbols.TermsAt.mapM {Struct : Symbols.Repr} [Syms : Symbols Struct] {m : Type → Type} {k : Nat} {R : Symbol.Repr} [Monad m] (terms : TermsAt k) (f : {α : Type} → [inst : IsSrt α] → Symbol.TermAt k α → m (R α)) : m (Struct R)

Equations

• terms.mapM f = Cvc.Symbols.mapM terms fun {α : Type} [Cvc.IsSrt α] => f

def Cvc.Symbols.TermsAt.map {Struct : Symbols.Repr} [Syms : Symbols Struct] {k : Nat} {R : Symbol.Repr} (terms : TermsAt k) (f : {α : Type} → [inst : IsSrt α] → Symbol.TermAt k α → R α) : Struct R

Equations

• terms.map f = terms.mapM fun {α : Type} [Cvc.IsSrt α] => f

def Cvc.Symbols.TermsAt.getModel {Struct : Symbols.Repr} [Syms : Symbols Struct] {k : Nat} (terms : TermsAt k) : Smt.Sat (ValuesAt k)

Retrieves the value of each symbol at some depth.

Equations

• terms.getModel = terms.mapM fun {α : Type} [Cvc.IsSrt α] => Cvc.Symbol.TermAt.getValue

def Cvc.Symbols.TermsAt.getValues {Struct : Symbols.Repr} [Syms : Symbols Struct] {k : Nat} (terms : TermsAt k) : Smt.Sat (ValuesAt k)

Retrieves the value of each symbol at some depth.

Equations

• @Cvc.Symbols.TermsAt.getValues = @Cvc.Symbols.TermsAt.getModel

def Cvc.State.AliasDsl.Idents.id_FunAtT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_FunAtT = Lean.mkIdent `FunAtT

def Cvc.State.AliasDsl.Idents.id_FunctionAtT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_FunctionAtT = Lean.mkIdent `FunctionAtT

def Cvc.State.AliasDsl.Idents.id_PredAtT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_PredAtT = Lean.mkIdent `PredAtT

def Cvc.State.AliasDsl.Idents.id_PredicateAtT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_PredicateAtT = Lean.mkIdent `PredicateAtT

def Cvc.State.AliasDsl.Idents.id_RelAtT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_RelAtT = Lean.mkIdent `RelAtT

def Cvc.State.AliasDsl.Idents.id_RelationAtT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_RelationAtT = Lean.mkIdent `RelationAtT

def Cvc.State.AliasDsl.Idents.id_FunAt : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_FunAt = Lean.mkIdent `FunAt

def Cvc.State.AliasDsl.Idents.id_FunctionAt : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_FunctionAt = Lean.mkIdent `FunctionAt

def Cvc.State.AliasDsl.Idents.id_PredAt : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_PredAt = Lean.mkIdent `PredAt

def Cvc.State.AliasDsl.Idents.id_PredicateAt : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_PredicateAt = Lean.mkIdent `PredicateAt

def Cvc.State.AliasDsl.Idents.id_RelAt : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_RelAt = Lean.mkIdent `RelAt

def Cvc.State.AliasDsl.Idents.id_RelationAt : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_RelationAt = Lean.mkIdent `RelationAt

def Cvc.State.AliasDsl.Idents.id_StatePredT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_StatePredT = Lean.mkIdent `StatePredT

def Cvc.State.AliasDsl.Idents.id_StatePredicateT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_StatePredicateT = Lean.mkIdent `StatePredicateT

def Cvc.State.AliasDsl.Idents.id_StateRelT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_StateRelT = Lean.mkIdent `StateRelT

def Cvc.State.AliasDsl.Idents.id_StateRelationT : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_StateRelationT = Lean.mkIdent `StateRelationT

def Cvc.State.AliasDsl.Idents.id_StatePred : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_StatePred = Lean.mkIdent `StatePred

def Cvc.State.AliasDsl.Idents.id_StatePredicate : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_StatePredicate = Lean.mkIdent `StatePredicate

def Cvc.State.AliasDsl.Idents.id_StateRel : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_StateRel = Lean.mkIdent `StateRel

def Cvc.State.AliasDsl.Idents.id_StateRelation : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_StateRelation = Lean.mkIdent `StateRelation

def Cvc.State.AliasDsl.Idents.id_k : Lean.Ident

Equations

• Cvc.State.AliasDsl.Idents.id_k = Lean.mkIdent `k

def Cvc.State.AliasDsl.aliasDsl : Lean.ParserDescr

Generates all Cvc.Symbols aliases.

Equations

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

def Cvc.State.AliasDsl.elabAliasDsl : Lean.Elab.Command.CommandElab

Generates all Cvc.Symbols aliases.

Equations

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