@[reducible, inline]

abbrev Cvc.ESys.ByName (depth : Nat := 0) : Type

Equations

• Cvc.ESys.ByName depth = Cvc.Sys Cvc.ESymbols.ByName.instState depth

def Cvc.ESys.ByName.mk (idents : ESymbols.ByName.Idents) (init : ESymbols.ByName.StatePred) (step : ESymbols.ByName.StateRel) : ByName

Equations

• Cvc.ESys.ByName.mk idents init step = Cvc.Sys.mk idents (fun {k : Nat} => init) fun {k : Nat} => step