Syntax extension for Cvc.Symbols specialized for unrolling

def Cvc.State.Dsl.stateTk : Lean.Parser.Parser

Equations

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

def Cvc.State.Dsl.stateStructure : Lean.Parser.Parser

Equations

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

def Cvc.State.Dsl.stateStructureSyntax : Lean.ParserDescr

Equations

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

def Cvc.State.Dsl.Idents.id_IdentsAt : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_IdentsAt = Lean.mkIdent `IdentsAt

def Cvc.State.Dsl.Idents.id_ValuesAt : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_ValuesAt = Lean.mkIdent `ValuesAt

def Cvc.State.Dsl.Idents.id_ModelAt : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_ModelAt = Lean.mkIdent `ModelAt

def Cvc.State.Dsl.Idents.id_TermsAt : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_TermsAt = Lean.mkIdent `TermsAt

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Cvc.State.Dsl.Idents.id_InvRelAt : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_InvRelAt = Lean.mkIdent `InvRelAt

def Cvc.State.Dsl.Idents.id_InvRelationAt : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_InvRelationAt = Lean.mkIdent `InvRelationAt

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Cvc.State.Dsl.Idents.id_unroll : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_unroll = Lean.mkIdent `unroll

def Cvc.State.Dsl.Idents.id_next : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_next = Lean.mkIdent `next

def Cvc.State.Dsl.Idents.id_declareAt : Lean.Ident

Equations

• Cvc.State.Dsl.Idents.id_declareAt = Lean.mkIdent `declareAt

def Cvc.State.Dsl.elabStateStructureSyntax : Lean.Elab.Command.CommandElab

Equations

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

Testing

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

Equations

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

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.ValuesAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.ValuesAt k✝ = Cvc.Symbols.ValuesAt k✝

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

Equations

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

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.IdentsAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.IdentsAt k✝ = Cvc.Symbols.IdentsAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.StateRelation : Type

Equations

• Cvc.State.Dsl.Test.MyState.StateRelation = Cvc.Symbols.StateRelation

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Relation : Type

Equations

• Cvc.State.Dsl.Test.MyState.Relation = Cvc.State.Dsl.Test.MyState.Rel

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.PredicateAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.PredicateAt k✝ = Cvc.Symbols.PredicateAt k✝

@[reducible, inline]

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

Equations

• Cvc.State.Dsl.Test.MyState.Function = Cvc.Symbols.Function

@[reducible, inline]

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

Equations

• Cvc.State.Dsl.Test.MyState.Fun = Cvc.Symbols.Fun

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Model : Type

Equations

• Cvc.State.Dsl.Test.MyState.Model = Cvc.Symbols.Model

@[reducible, inline]

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

Equations

• Cvc.State.Dsl.Test.MyState.FunAt k✝ = Cvc.Symbols.FunAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.idents : Idents

Equations

• Cvc.State.Dsl.Test.MyState.idents = { myCounter := Cvc.Symbol.mkIdent "myCounter", myReset := Cvc.Symbol.mkIdent "myReset" }

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Rel : Type

Equations

• Cvc.State.Dsl.Test.MyState.Rel = Cvc.Symbols.Rel

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Values : Type

Equations

• Cvc.State.Dsl.Test.MyState.Values = Cvc.Symbols.Values

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.toSymbols : Symbols MyState

Equations

• Cvc.State.Dsl.Test.MyState.toSymbols = Cvc.State.Dsl.Test.MyState.instSymbols

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.StatePred : Type

Equations

• Cvc.State.Dsl.Test.MyState.StatePred = Cvc.Symbols.StatePred

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.RelationAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.RelationAt k✝ = Cvc.Symbols.RelationAt k✝

@[reducible, inline]

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

Equations

• Cvc.State.Dsl.Test.MyState.next idents✝ = Cvc.Symbols.next idents✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.InvRelationAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.InvRelationAt k✝ = Cvc.Symbols.InvRelationAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.StatePredicate : Type

Equations

• Cvc.State.Dsl.Test.MyState.StatePredicate = Cvc.Symbols.StatePredicate

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.TermsAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.TermsAt k✝ = Cvc.Symbols.TermsAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.StateRel : Type

Equations

• Cvc.State.Dsl.Test.MyState.StateRel = Cvc.Symbols.StateRel

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

Testing...

• myCounter : R Int
• myReset : R Bool

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Spec : Symbols MyState

Equations

• Cvc.State.Dsl.Test.MyState.Spec = Cvc.State.Dsl.Test.MyState.instSymbols

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.PredAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.PredAt k✝ = Cvc.Symbols.PredAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Predicate : Type

Equations

• Cvc.State.Dsl.Test.MyState.Predicate = Cvc.State.Dsl.Test.MyState.Pred

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Idents : Type

Equations

• Cvc.State.Dsl.Test.MyState.Idents = Cvc.Symbols.Idents

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.ModelAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.ModelAt k✝ = Cvc.Symbols.ModelAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.RelAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.RelAt k✝ = Cvc.Symbols.RelAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.InvRelAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.MyState.InvRelAt k✝ = Cvc.Symbols.InvRelAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Terms : Type

Equations

• Cvc.State.Dsl.Test.MyState.Terms = Cvc.Symbols.Terms

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.MyState.Pred : Type

Equations

• Cvc.State.Dsl.Test.MyState.Pred = Cvc.Symbols.Pred

@[reducible, inline]

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

Equations

• Cvc.State.Dsl.Test.MyState.FunctionAt k✝ = Cvc.Symbols.FunctionAt k✝

@[defaultInstance 1000]

instance Cvc.State.Dsl.Test.MyState.instSymbols : Symbols MyState

Equations

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

def Cvc.State.Dsl.Test.My.State.myCounter! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Int) β✝] : State R✝ → β✝

Equations

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

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.TermsAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.TermsAt k✝ = Cvc.Symbols.TermsAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Values : Type

Equations

• Cvc.State.Dsl.Test.My.State.Values = Cvc.Symbols.Values

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Relation : Type

Equations

• Cvc.State.Dsl.Test.My.State.Relation = Cvc.State.Dsl.Test.My.State.Rel

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Function (α : Type) : Type

Equations

• Cvc.State.Dsl.Test.My.State.Function = Cvc.Symbols.Function

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Predicate : Type

Equations

• Cvc.State.Dsl.Test.My.State.Predicate = Cvc.State.Dsl.Test.My.State.Pred

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Terms : Type

Equations

• Cvc.State.Dsl.Test.My.State.Terms = Cvc.Symbols.Terms

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.StatePredicate : Type

Equations

• Cvc.State.Dsl.Test.My.State.StatePredicate = Cvc.Symbols.StatePredicate

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.RelAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.RelAt k✝ = Cvc.Symbols.RelAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.declareAt : Idents → (k : optParam Nat 0) → Smt (TermsAt k)

Equations

• Cvc.State.Dsl.Test.My.State.declareAt idents✝ k✝ = Cvc.Symbols.declareAt idents✝ k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.unroll : Idents → (k : optParam Nat 0) → IdentsAt k

Equations

• Cvc.State.Dsl.Test.My.State.unroll idents✝ k✝ = Cvc.Symbols.unroll idents✝ k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Pred : Type

Equations

• Cvc.State.Dsl.Test.My.State.Pred = Cvc.Symbols.Pred

structure Cvc.State.Dsl.Test.My.State (R : Symbol.Repr) : Type

Testing names featuring .-separators.

• myCounter : R Int
• myReset : R Bool

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.idents : Idents

Equations

• Cvc.State.Dsl.Test.My.State.idents = { myCounter := Cvc.Symbol.mkIdent "myCounter", myReset := Cvc.Symbol.mkIdent "myReset" }

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Idents : Type

Equations

• Cvc.State.Dsl.Test.My.State.Idents = Cvc.Symbols.Idents

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.RelationAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.RelationAt k✝ = Cvc.Symbols.RelationAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.toSymbols : Symbols State

Equations

• Cvc.State.Dsl.Test.My.State.toSymbols = Cvc.State.Dsl.Test.My.State.instSymbols

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.FunctionAt : Nat → (α : Type) → Type

Equations

• Cvc.State.Dsl.Test.My.State.FunctionAt k✝ = Cvc.Symbols.FunctionAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.next {k✝ : Nat} : IdentsAt k✝ → IdentsAt k✝.succ

Equations

• Cvc.State.Dsl.Test.My.State.next idents✝ = Cvc.Symbols.next idents✝

@[defaultInstance 1000]

instance Cvc.State.Dsl.Test.My.State.instSymbols : Symbols State

Equations

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

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Rel : Type

Equations

• Cvc.State.Dsl.Test.My.State.Rel = Cvc.Symbols.Rel

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Model : Type

Equations

• Cvc.State.Dsl.Test.My.State.Model = Cvc.Symbols.Model

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.InvRelationAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.InvRelationAt k✝ = Cvc.Symbols.InvRelationAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.StateRelation : Type

Equations

• Cvc.State.Dsl.Test.My.State.StateRelation = Cvc.Symbols.StateRelation

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.ModelAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.ModelAt k✝ = Cvc.Symbols.ModelAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.IdentsAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.IdentsAt k✝ = Cvc.Symbols.IdentsAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.PredAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.PredAt k✝ = Cvc.Symbols.PredAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Spec : Symbols State

Equations

• Cvc.State.Dsl.Test.My.State.Spec = Cvc.State.Dsl.Test.My.State.instSymbols

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.PredicateAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.PredicateAt k✝ = Cvc.Symbols.PredicateAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.FunAt : Nat → (α : Type) → Type

Equations

• Cvc.State.Dsl.Test.My.State.FunAt k✝ = Cvc.Symbols.FunAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.Fun (α : Type) : Type

Equations

• Cvc.State.Dsl.Test.My.State.Fun = Cvc.Symbols.Fun

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.StateRel : Type

Equations

• Cvc.State.Dsl.Test.My.State.StateRel = Cvc.Symbols.StateRel

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.ValuesAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.ValuesAt k✝ = Cvc.Symbols.ValuesAt k✝

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.StatePred : Type

Equations

• Cvc.State.Dsl.Test.My.State.StatePred = Cvc.Symbols.StatePred

def Cvc.State.Dsl.Test.My.State.myReset! {R✝ : Symbol.Repr} {β✝ : Type} [Symbol.Getter (R✝ Bool) β✝] : State R✝ → β✝

Equations

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

@[reducible, inline]

abbrev Cvc.State.Dsl.Test.My.State.InvRelAt : Nat → Type

Equations

• Cvc.State.Dsl.Test.My.State.InvRelAt k✝ = Cvc.Symbols.InvRelAt k✝