@[reducible, inline]

abbrev Cvc.ESymbol.IdentAt (k : Nat) : Type

Equations

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

@[reducible, inline]

abbrev Cvc.ESymbol.TermAt (k : Nat) : Type

Equations

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

@[reducible, inline]

abbrev Cvc.ESymbol.ValueAt (k : Nat) : Type

Equations

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

def Cvc.ESymbol.unrollAt (ident : ESymbol.Ident) (k : Nat := 0) : IdentAt k

Equations

• Cvc.ESymbol.unrollAt ident k = Cvc.ESymbol.map ident fun (x : Cvc.Symbol.Ident (ident.srt fun (x : Type) [Cvc.IsSrt x] => Cvc.Symbol.Ident x).toType) => x.unroll k

instance Cvc.ESymbol.instToStringIdentAt {k : Nat} : ToString (IdentAt k)

Equations

• Cvc.ESymbol.instToStringIdentAt = { toString := fun (id : Cvc.ESymbol.IdentAt k) => toString id.getData }

instance Cvc.ESymbol.instToStringTermAt {k : Nat} : ToString (TermAt k)

Equations

• Cvc.ESymbol.instToStringTermAt = { toString := fun (id : Cvc.ESymbol.TermAt k) => toString id.getData }

instance Cvc.ESymbol.instToStringValueAt {k : Nat} : ToString (ValueAt k)

Equations

• Cvc.ESymbol.instToStringValueAt = { toString := fun (id : Cvc.ESymbol.ValueAt k) => toString id.getData }

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.instState : Symbols ByName

Equations

• Cvc.ESymbols.ByName.instState = Cvc.ESymbols.ByName.instSymbols

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.IdentsAt (k : Nat) : Type

Equations

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

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.TermsAt (k : Nat) : Type

Equations

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

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.ValuesAt (k : Nat) : Type

Equations

• Cvc.ESymbols.ByName.ValuesAt k = Cvc.ESymbols.ByName fun (x : Type) [Cvc.IsSrt x] => Cvc.Symbol.ValueAt k x

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.RelAtT (m : Type → Type u_1) (k : Nat) : Type u_1

Equations

• Cvc.ESymbols.ByName.RelAtT m k = (Cvc.ESymbols.ByName.TermsAt k → Cvc.ESymbols.ByName.PredAtT m k.succ)

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.RelationAt (k : Nat) : Type

Equations

• Cvc.ESymbols.ByName.RelationAt k = Cvc.ESymbols.ByName.RelAtT Id k

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.FunAt (α : Type) (k : Nat) : Type

Equations

• Cvc.ESymbols.ByName.FunAt α k = Cvc.ESymbols.ByName.FunAtT Id α k

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.StatePredT (m : Type → Type u_1) : Type u_1

Equations

• Cvc.ESymbols.ByName.StatePredT m = ({k : Nat} → Cvc.ESymbols.ByName.PredAtT m k)

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.FunctionAtT (m : Type → Type u_1) (α : Type) (k : Nat) : Type u_1

Equations

• Cvc.ESymbols.ByName.FunctionAtT = Cvc.ESymbols.ByName.FunAtT

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.StateRelationT (m : Type → Type u_1) : Type u_1

Equations

• Cvc.ESymbols.ByName.StateRelationT m = ({k : Nat} → Cvc.ESymbols.ByName.PredAtT m k)

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.StatePred : Type

Equations

• Cvc.ESymbols.ByName.StatePred = Cvc.ESymbols.ByName.StatePredT Id

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.PredicateAtT (m : Type → Type u_1) (k : Nat) : Type u_1

Equations

• Cvc.ESymbols.ByName.PredicateAtT m k = Cvc.ESymbols.ByName.FunAtT m Bool k

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.RelationAtT (m : Type → Type u_1) (k : Nat) : Type u_1

Equations

• Cvc.ESymbols.ByName.RelationAtT m k = (Cvc.ESymbols.ByName.TermsAt k → Cvc.ESymbols.ByName.PredAtT m k.succ)

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.PredicateAt (k : Nat) : Type

Equations

• Cvc.ESymbols.ByName.PredicateAt k = Cvc.ESymbols.ByName.PredAtT Id k

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.FunAtT (m : Type → Type u_1) (α : Type) (k : Nat) : Type u_1

Equations

• Cvc.ESymbols.ByName.FunAtT m α k = (Cvc.ESymbols.ByName.TermsAt k → Cvc.Term.BuildT m (Cvc.Term α))

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.PredAtT (m : Type → Type u_1) (k : Nat) : Type u_1

Equations

• Cvc.ESymbols.ByName.PredAtT m k = Cvc.ESymbols.ByName.FunAtT m Bool k

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.StatePredicate : Type

Equations

• Cvc.ESymbols.ByName.StatePredicate = Cvc.ESymbols.ByName.StatePredT Id

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.RelAt (k : Nat) : Type

Equations

• Cvc.ESymbols.ByName.RelAt k = Cvc.ESymbols.ByName.RelAtT Id k

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.FunctionAt (α : Type) (k : Nat) : Type

Equations

• Cvc.ESymbols.ByName.FunctionAt α k = Cvc.ESymbols.ByName.FunAtT Id α k

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.StatePredicateT (m : Type → Type u_1) : Type u_1

Equations

• Cvc.ESymbols.ByName.StatePredicateT m = ({k : Nat} → Cvc.ESymbols.ByName.PredAtT m k)

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.StateRel : Type

Equations

• Cvc.ESymbols.ByName.StateRel = Cvc.ESymbols.ByName.StateRelT Id

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.StateRelT (m : Type → Type u_1) : Type u_1

Equations

• Cvc.ESymbols.ByName.StateRelT m = ({k : Nat} → Cvc.ESymbols.ByName.RelAtT m k)

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.PredAt (k : Nat) : Type

Equations

• Cvc.ESymbols.ByName.PredAt k = Cvc.ESymbols.ByName.PredAtT Id k

@[reducible, inline]

abbrev Cvc.ESymbols.ByName.StateRelation : Type

Equations

• Cvc.ESymbols.ByName.StateRelation = Cvc.ESymbols.ByName.StateRelT Id