def Cvc.Sys.Dsl.systemTk : Lean.Parser.Parser

Equations

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

def Cvc.Sys.Dsl.Idents.id_instState : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.id_instState = Lean.mkIdent `instState

def Cvc.Sys.Dsl.Idents.id_ofIdents : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.id_ofIdents = Lean.mkIdent `ofIdents

def Cvc.Sys.Dsl.Idents.id_mk : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.id_mk = Lean.mkIdent `mk

def Cvc.Sys.Dsl.Idents.id_init : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.id_init = Lean.mkIdent `init

def Cvc.Sys.Dsl.Idents.id_step : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.id_step = Lean.mkIdent `step

def Cvc.Sys.Dsl.Idents.id_candidates : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.id_candidates = Lean.mkIdent `namedCandidates

def Cvc.Sys.Dsl.Idents.idRef_Sys : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.idRef_Sys = Lean.mkIdent `Cvc.Sys

def Cvc.Sys.Dsl.Idents.idRef_Sys_mk : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.idRef_Sys_mk = Lean.mkIdent `Cvc.Sys.mk

def Cvc.Sys.Dsl.Idents.idRef_Smt : Lean.Ident

Equations

• Cvc.Sys.Dsl.Idents.idRef_Smt = Lean.mkIdent `Cvc.Smt

def Cvc.Sys.Dsl.systemForDefSyntax : Lean.ParserDescr

Equations

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

def Cvc.Sys.Dsl.elabSystemForDefSyntax : Lean.Elab.Command.CommandElab

Equations

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

def Cvc.Sys.Dsl.systemWithDefSyntax : Lean.ParserDescr

Equations

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

def Cvc.Sys.Dsl.elabSystemWithDefSyntax : Lean.Elab.Command.CommandElab

Equations

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

Testing

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Terms : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Terms = Cvc.Symbols.Terms

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Pred : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Pred = Cvc.Symbols.Pred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.RelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.RelAt k✝ = Cvc.Symbols.RelAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Values : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Values = Cvc.Symbols.Values

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Idents : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Idents = Cvc.Symbols.Idents

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.ValuesAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.ValuesAt k✝ = Cvc.Symbols.ValuesAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.RelationAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.RelationAt k✝ = Cvc.Symbols.RelationAt k✝

def Cvc.Sys.Dsl.Test.For.MyState.bVar! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Bool) β✝] : MyState R✝ → β✝

Equations

• self✝.bVar! = Cvc.Symbol.Getter.getInner self✝.bVar

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Model : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Model = Cvc.Symbols.Model

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.PredicateAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.PredicateAt k✝ = Cvc.Symbols.PredicateAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.unroll : Idents → (k : optParam Nat 0) → IdentsAt k

Equations

• Cvc.Sys.Dsl.Test.For.MyState.unroll idents✝ k✝ = Cvc.Symbols.unroll idents✝ k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.StatePredicate : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.StatePredicate = Cvc.Symbols.StatePredicate

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.StateRel : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.StateRel = Cvc.Symbols.StateRel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.declareAt : Idents → (k : optParam Nat 0) → Smt (TermsAt k)

Equations

• Cvc.Sys.Dsl.Test.For.MyState.declareAt idents✝ k✝ = Cvc.Symbols.declareAt idents✝ k✝

@[defaultInstance 1000]

instance Cvc.Sys.Dsl.Test.For.MyState.instSymbols : Symbols MyState

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Function (α : Type) : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Function = Cvc.Symbols.Function

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Predicate : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Predicate = Cvc.Sys.Dsl.Test.For.MyState.Pred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.next {k✝ : Nat} : IdentsAt k✝ → IdentsAt k✝.succ

Equations

• Cvc.Sys.Dsl.Test.For.MyState.next idents✝ = Cvc.Symbols.next idents✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.PredAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.PredAt k✝ = Cvc.Symbols.PredAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.FunAt : Nat → (α : Type) → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.FunAt k✝ = Cvc.Symbols.FunAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Rel : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Rel = Cvc.Symbols.Rel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.ModelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.ModelAt k✝ = Cvc.Symbols.ModelAt k✝

def Cvc.Sys.Dsl.Test.For.MyState.intVar! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Int) β✝] : MyState R✝ → β✝

Equations

• self✝.intVar! = Cvc.Symbol.Getter.getInner self✝.intVar

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.StatePred : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.StatePred = Cvc.Symbols.StatePred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.InvRelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.InvRelAt k✝ = Cvc.Symbols.InvRelAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Relation : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Relation = Cvc.Sys.Dsl.Test.For.MyState.Rel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Spec : Symbols MyState

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Spec = Cvc.Sys.Dsl.Test.For.MyState.instSymbols

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.idents : Idents

Equations

• Cvc.Sys.Dsl.Test.For.MyState.idents = { bVar := Cvc.Symbol.mkIdent "bVar", intVar := Cvc.Symbol.mkIdent "intVar" }

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.IdentsAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.IdentsAt k✝ = Cvc.Symbols.IdentsAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.InvRelationAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.InvRelationAt k✝ = Cvc.Symbols.InvRelationAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.StateRelation : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.StateRelation = Cvc.Symbols.StateRelation

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.FunctionAt : Nat → (α : Type) → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.FunctionAt k✝ = Cvc.Symbols.FunctionAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.TermsAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.TermsAt k✝ = Cvc.Symbols.TermsAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.Fun (α : Type) : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState.Fun = Cvc.Symbols.Fun

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState.toSymbols : Symbols MyState

Equations

• Cvc.Sys.Dsl.Test.For.MyState.toSymbols = Cvc.Sys.Dsl.Test.For.MyState.instSymbols

structure Cvc.Sys.Dsl.Test.For.MyState (R : Symbol.Repr) : Type

State structure.

• bVar : R Bool
• intVar : R Int

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys.StateRel : Type

Equations

• Cvc.Sys.Dsl.Test.For.MySys.StateRel = Cvc.Symbols.StateRel

def Cvc.Sys.Dsl.Test.For.MySys.instState : Symbols MyState

Equations

• Cvc.Sys.Dsl.Test.For.MySys.instState = inferInstance

def Cvc.Sys.Dsl.Test.For.MySys.ofIdents : Symbols.Idents → MySys

Constructor.

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys : optParam Nat 0 → Type

MyState- System.

Equations

• Cvc.Sys.Dsl.Test.For.MySys depth✝ = Cvc.Sys Cvc.Sys.Dsl.Test.For.MySys.instState depth✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys.StateRelation : Type

Equations

• Cvc.Sys.Dsl.Test.For.MySys.StateRelation = Cvc.Symbols.StateRelation

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys.StatePredicate : Type

Equations

• Cvc.Sys.Dsl.Test.For.MySys.StatePredicate = Cvc.Symbols.StatePredicate

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys.StatePred : Type

Equations

• Cvc.Sys.Dsl.Test.For.MySys.StatePred = Cvc.Symbols.StatePred

def Cvc.Sys.Dsl.Test.For.MySys.ofIdents.init {k : Nat} : Symbols.TermsAt k → Term.BuildT Id (Term Bool)

Equations

• Cvc.Sys.Dsl.Test.For.MySys.ofIdents.init state = do let __do_lift ← Cvc.Term.int 0 let __do_lift_1 ← pure state.intVar Cvc.Term.le __do_lift __do_lift_1.getSymbol.get

def Cvc.Sys.Dsl.Test.For.MySys.ofIdents.step {k : Nat} : Symbols.TermsAt k → Symbols.TermsAt k.succ → Term.BuildT Id (Term Bool)

Equations

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

def Cvc.Sys.Dsl.Test.For.MySys.ofIdents.namedCandidates : Symbols.NamedPredicates

Equations

• Cvc.Sys.Dsl.Test.For.MySys.ofIdents.namedCandidates = Cvc.RBMap.empty

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Predicate : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Predicate = Cvc.Sys.Dsl.Test.For.MyState'.Pred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.StatePred : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.StatePred = Cvc.Symbols.StatePred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.unroll : Idents → (k : optParam Nat 0) → IdentsAt k

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.unroll idents✝ k✝ = Cvc.Symbols.unroll idents✝ k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Terms : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Terms = Cvc.Symbols.Terms

def Cvc.Sys.Dsl.Test.For.MyState'.intVar! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Int) β✝] : MyState' R✝ → β✝

Equations

• self✝.intVar! = Cvc.Symbol.Getter.getInner self✝.intVar

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Model : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Model = Cvc.Symbols.Model

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Idents : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Idents = Cvc.Symbols.Idents

def Cvc.Sys.Dsl.Test.For.MyState'.bVar! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Bool) β✝] : MyState' R✝ → β✝

Equations

• self✝.bVar! = Cvc.Symbol.Getter.getInner self✝.bVar

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Fun (α : Type) : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Fun = Cvc.Symbols.Fun

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.toSymbols : Symbols MyState'

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.toSymbols = Cvc.Sys.Dsl.Test.For.MyState'.instSymbols

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Spec : Symbols MyState'

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Spec = Cvc.Sys.Dsl.Test.For.MyState'.instSymbols

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.ModelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.ModelAt k✝ = Cvc.Symbols.ModelAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.PredAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.PredAt k✝ = Cvc.Symbols.PredAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.FunctionAt : Nat → (α : Type) → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.FunctionAt k✝ = Cvc.Symbols.FunctionAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.FunAt : Nat → (α : Type) → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.FunAt k✝ = Cvc.Symbols.FunAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.RelationAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.RelationAt k✝ = Cvc.Symbols.RelationAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.InvRelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.InvRelAt k✝ = Cvc.Symbols.InvRelAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.next {k✝ : Nat} : IdentsAt k✝ → IdentsAt k✝.succ

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.next idents✝ = Cvc.Symbols.next idents✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.TermsAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.TermsAt k✝ = Cvc.Symbols.TermsAt k✝

structure Cvc.Sys.Dsl.Test.For.MyState' (R : Symbol.Repr) : Type

State structure.

• bVar : R Bool
• intVar : R Int

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.declareAt : Idents → (k : optParam Nat 0) → Smt (TermsAt k)

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.declareAt idents✝ k✝ = Cvc.Symbols.declareAt idents✝ k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.ValuesAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.ValuesAt k✝ = Cvc.Symbols.ValuesAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.StateRel : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.StateRel = Cvc.Symbols.StateRel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.StatePredicate : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.StatePredicate = Cvc.Symbols.StatePredicate

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.PredicateAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.PredicateAt k✝ = Cvc.Symbols.PredicateAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.idents : Idents

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.idents = { bVar := Cvc.Symbol.mkIdent "bVar", intVar := Cvc.Symbol.mkIdent "intVar" }

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Rel : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Rel = Cvc.Symbols.Rel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Function (α : Type) : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Function = Cvc.Symbols.Function

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.RelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.RelAt k✝ = Cvc.Symbols.RelAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Values : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Values = Cvc.Symbols.Values

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Pred : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Pred = Cvc.Symbols.Pred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.Relation : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.Relation = Cvc.Sys.Dsl.Test.For.MyState'.Rel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.StateRelation : Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.StateRelation = Cvc.Symbols.StateRelation

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.InvRelationAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.InvRelationAt k✝ = Cvc.Symbols.InvRelationAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MyState'.IdentsAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.For.MyState'.IdentsAt k✝ = Cvc.Symbols.IdentsAt k✝

@[defaultInstance 1000]

instance Cvc.Sys.Dsl.Test.For.MyState'.instSymbols : Symbols MyState'

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys' : optParam Nat 0 → Type

MyState- System.

Equations

• Cvc.Sys.Dsl.Test.For.MySys' depth✝ = Cvc.Sys Cvc.Sys.Dsl.Test.For.MySys'.instState depth✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys'.StateRelation : Type

Equations

• Cvc.Sys.Dsl.Test.For.MySys'.StateRelation = Cvc.Symbols.StateRelation

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys'.StatePred : Type

Equations

• Cvc.Sys.Dsl.Test.For.MySys'.StatePred = Cvc.Symbols.StatePred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys'.StateRel : Type

Equations

• Cvc.Sys.Dsl.Test.For.MySys'.StateRel = Cvc.Symbols.StateRel

def Cvc.Sys.Dsl.Test.For.MySys'.instState : Symbols MyState

Equations

• Cvc.Sys.Dsl.Test.For.MySys'.instState = inferInstance

def Cvc.Sys.Dsl.Test.For.MySys'.ofIdents : Symbols.Idents → MySys'

Constructor.

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.For.MySys'.StatePredicate : Type

Equations

• Cvc.Sys.Dsl.Test.For.MySys'.StatePredicate = Cvc.Symbols.StatePredicate

def Cvc.Sys.Dsl.Test.For.MySys'.ofIdents.init {k : Nat} : Symbols.TermsAt k → Term.BuildT Id (Term Bool)

Equations

• Cvc.Sys.Dsl.Test.For.MySys'.ofIdents.init state = do let __do_lift ← Cvc.Term.int 0 let __do_lift_1 ← pure state.intVar Cvc.Term.le __do_lift __do_lift_1.getSymbol.get

def Cvc.Sys.Dsl.Test.For.MySys'.ofIdents.step {k : Nat} : Symbols.TermsAt k → Symbols.TermsAt k.succ → Term.BuildT Id (Term Bool)

Equations

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

def Cvc.Sys.Dsl.Test.For.MySys'.ofIdents.namedCandidates : RBMap String ({k : Nat} → Symbols.TermsAt k → Term.BuildT Id (Term Bool))

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.PredicateAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.PredicateAt k✝ = Cvc.Symbols.PredicateAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.TermsAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.TermsAt k✝ = Cvc.Symbols.TermsAt k✝

def Cvc.Sys.Dsl.Test.With.MyState.intVar! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Int) β✝] : MyState R✝ → β✝

Equations

• self✝.intVar! = Cvc.Symbol.Getter.getInner self✝.intVar

def Cvc.Sys.Dsl.Test.With.MyState.bVar! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Bool) β✝] : MyState R✝ → β✝

Equations

• self✝.bVar! = Cvc.Symbol.Getter.getInner self✝.bVar

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.StatePred : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.StatePred = Cvc.Symbols.StatePred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.StateRelation : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.StateRelation = Cvc.Symbols.StateRelation

@[defaultInstance 1000]

instance Cvc.Sys.Dsl.Test.With.MyState.instSymbols : Symbols MyState

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Rel : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Rel = Cvc.Symbols.Rel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.StatePredicate : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.StatePredicate = Cvc.Symbols.StatePredicate

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Values : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Values = Cvc.Symbols.Values

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Pred : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Pred = Cvc.Symbols.Pred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.unroll : Idents → (k : optParam Nat 0) → IdentsAt k

Equations

• Cvc.Sys.Dsl.Test.With.MyState.unroll idents✝ k✝ = Cvc.Symbols.unroll idents✝ k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Idents : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Idents = Cvc.Symbols.Idents

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.idents : Idents

Equations

• Cvc.Sys.Dsl.Test.With.MyState.idents = { bVar := Cvc.Symbol.mkIdent "bVar", intVar := Cvc.Symbol.mkIdent "intVar" }

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Model : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Model = Cvc.Symbols.Model

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.PredAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.PredAt k✝ = Cvc.Symbols.PredAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Terms : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Terms = Cvc.Symbols.Terms

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Predicate : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Predicate = Cvc.Sys.Dsl.Test.With.MyState.Pred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.ModelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.ModelAt k✝ = Cvc.Symbols.ModelAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.next {k✝ : Nat} : IdentsAt k✝ → IdentsAt k✝.succ

Equations

• Cvc.Sys.Dsl.Test.With.MyState.next idents✝ = Cvc.Symbols.next idents✝

def Cvc.Sys.Dsl.Test.With.MySys.idents : MyState.Idents

Equations

• Cvc.Sys.Dsl.Test.With.MySys.idents = Cvc.Sys.Dsl.Test.With.MyState.idents

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MySys.StateRelation : Type

Equations

• Cvc.Sys.Dsl.Test.With.MySys.StateRelation = Cvc.Symbols.StateRelation

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MySys.StateRel : Type

Equations

• Cvc.Sys.Dsl.Test.With.MySys.StateRel = Cvc.Symbols.StateRel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MySys : optParam Nat 0 → Type

MyState-system.

Equations

• Cvc.Sys.Dsl.Test.With.MySys depth✝ = Cvc.Sys Cvc.Sys.Dsl.Test.With.MySys.instState depth✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.IdentsAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.IdentsAt k✝ = Cvc.Symbols.IdentsAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.FunctionAt : Nat → (α : Type) → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.FunctionAt k✝ = Cvc.Symbols.FunctionAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Fun (α : Type) : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Fun = Cvc.Symbols.Fun

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.InvRelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.InvRelAt k✝ = Cvc.Symbols.InvRelAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Relation : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Relation = Cvc.Sys.Dsl.Test.With.MyState.Rel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.RelationAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.RelationAt k✝ = Cvc.Symbols.RelationAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Function (α : Type) : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Function = Cvc.Symbols.Function

def Cvc.Sys.Dsl.Test.With.MySys.ofIdents : Symbols.Idents → MySys

Constructor.

Equations

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

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.InvRelationAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.InvRelationAt k✝ = Cvc.Symbols.InvRelationAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.toSymbols : Symbols MyState

Equations

• Cvc.Sys.Dsl.Test.With.MyState.toSymbols = Cvc.Sys.Dsl.Test.With.MyState.instSymbols

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.StateRel : Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.StateRel = Cvc.Symbols.StateRel

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MySys.StatePred : Type

Equations

• Cvc.Sys.Dsl.Test.With.MySys.StatePred = Cvc.Symbols.StatePred

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MySys.StatePredicate : Type

Equations

• Cvc.Sys.Dsl.Test.With.MySys.StatePredicate = Cvc.Symbols.StatePredicate

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.ValuesAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.ValuesAt k✝ = Cvc.Symbols.ValuesAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.Spec : Symbols MyState

Equations

• Cvc.Sys.Dsl.Test.With.MyState.Spec = Cvc.Sys.Dsl.Test.With.MyState.instSymbols

def Cvc.Sys.Dsl.Test.With.MySys.mk : MySys

Equations

• Cvc.Sys.Dsl.Test.With.MySys.mk = Cvc.Sys.Dsl.Test.With.MySys.ofIdents Cvc.Sys.Dsl.Test.With.MySys.idents

def Cvc.Sys.Dsl.Test.With.MySys.instState : Symbols MyState

Equations

• Cvc.Sys.Dsl.Test.With.MySys.instState = inferInstance

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.FunAt : Nat → (α : Type) → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.FunAt k✝ = Cvc.Symbols.FunAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.RelAt : Nat → Type

Equations

• Cvc.Sys.Dsl.Test.With.MyState.RelAt k✝ = Cvc.Symbols.RelAt k✝

@[reducible, inline]

abbrev Cvc.Sys.Dsl.Test.With.MyState.declareAt : Idents → (k : optParam Nat 0) → Smt (TermsAt k)

Equations

• Cvc.Sys.Dsl.Test.With.MyState.declareAt idents✝ k✝ = Cvc.Symbols.declareAt idents✝ k✝

structure Cvc.Sys.Dsl.Test.With.MyState (R : Symbol.Repr) : Type

State structure.

• bVar : R Bool
• intVar : R Int

def Cvc.Sys.Dsl.Test.With.MySys.ofIdents.init {k : Nat} : Symbols.TermsAt k → Term.BuildT Id (Term Bool)

Equations

• Cvc.Sys.Dsl.Test.With.MySys.ofIdents.init state = do let __do_lift ← Cvc.Term.int 0 let __do_lift_1 ← pure state.intVar Cvc.Term.le __do_lift __do_lift_1.getSymbol.get

def Cvc.Sys.Dsl.Test.With.MySys.ofIdents.step {k : Nat} : Symbols.TermsAt k → Symbols.TermsAt k.succ → Term.BuildT Id (Term Bool)

Equations

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

def Cvc.Sys.Dsl.Test.With.MySys.ofIdents.namedCandidates : Symbols.NamedPredicates

Equations

• Cvc.Sys.Dsl.Test.With.MySys.ofIdents.namedCandidates = Cvc.RBMap.empty