Library setup: re-exports and helpers

@[reducible, inline]

abbrev Cvc.𝕂 {α : Sort u_1} {β : Sort u_2} (val : α) : β → α

The constant combinator.

Equations

• Cvc.𝕂 val x✝ = val

@[reducible, inline]

abbrev Cvc.RBMap (α β : Type) [Ord α] : Type

Equations

• Cvc.RBMap α β = Batteries.RBMap α β compare

def Cvc.RBMap.empty {α : Type} [Ord α] {β : Type} : RBMap α β

The empty map.

Equations

• Cvc.RBMap.empty = Batteries.RBMap.empty

def Cvc.RBMap.ofList {α : Type} [Ord α] {β : Type} : List (α × β) → RBMap α β

Builds a map from a list.

Equations

• Cvc.RBMap.ofList x✝ = Batteries.RBMap.ofList x✝ compare

def Cvc.RBMap.filter {α : Type} [Ord α] {β : Type} (map : RBMap α β) (f : α → β → Bool) : RBMap α β

Removes from map the bindings key/val such that ¬ f key val.

Equations

• Cvc.RBMap.filter = Batteries.RBMap.filter

def Cvc.RBMap.filterVal {α : Type} [Ord α] {β : Type} (map : RBMap α β) (f : β → Bool) : RBMap α β

Removes from map the bindings key/val such that ¬ f val.

Equations

• map.filterVal f = map.filter fun (x : α) => f

def Cvc.RBMap.insert {α : Type} [Ord α] {β : Type} (map : RBMap α β) (key : α) (val : β) : RBMap α β

Inserts a key/val binding in a map.

See also RBMap.insert'.

Equations

• Cvc.RBMap.insert = Batteries.RBMap.insert

def Cvc.RBMap.insert' {α : Type} [Ord α] {β : Type} (map : RBMap α β) (key : α) (val : β) : Option β × RBMap α β

Adds a key/val binding in a map, returns the previous value of key if any.

See also RBMap.insert.

Equations

• map.insert' key val = (Batteries.RBMap.find? map key, map.insert key val)

def Cvc.RBMap.insertNew? {α : Type} [Ord α] {β : Type} (map : RBMap α β) (key : α) (val : β) : Option (RBMap α β)

Adds a key/val binding in a map, none if a binding for key already exists.

Equations

• map.insertNew? key val = match map.insert' key val with | (prev?, map) => Option.map (Cvc.𝕂 map) prev?

def Cvc.RBMap.erase {α : Type} [Ord α] {β : Type} (map : RBMap α β) (key : α) : RBMap α β

Removes from map the binding for key, if any.

See also RBMap.erase'.

Equations

• Cvc.RBMap.erase = Batteries.RBMap.erase

def Cvc.RBMap.erase' {α : Type} [Ord α] {β : Type} (map : RBMap α β) (key : α) : Option β × RBMap α β

Removes a key/val binding from a map, yields some val if such a binding existed.

See also RBMap.erase.

Equations

• map.erase' key = (Batteries.RBMap.find? map key, map.erase key)

def Cvc.RBMap.eraseExisting? {α : Type} [Ord α] {β : Type} (map : RBMap α β) (key : α) : Option (RBMap α β)

Removes a key/val binding from a map, none if no binding for key existed.

Equations

• map.eraseExisting? key = match map.erase' key with | (some val, map) => some map | (none, snd) => none

def Cvc.RBMap.mapVal {α : Type} [Ord α] {β γ : Type} (f : α → β → γ) (map : RBMap α β) : RBMap α γ

Map over the values of a map.

Equations

• Cvc.RBMap.mapVal = Batteries.RBMap.mapVal

def Cvc.RBMap.filterMapValM {α : Type} [Ord α] {m : Type → Type u_1} {β γ : Type} [Monad m] (f : α → β → m (Option γ)) (map : RBMap α β) : m (RBMap α γ)

Monadic filter/map over the values of a map.

Equations

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

def Cvc.RBMap.mapValM {α : Type} [Ord α] {m : Type → Type u_1} {β γ : Type} [Monad m] (f : α → β → m γ) (map : RBMap α β) : m (RBMap α γ)

Monadic map over the values of a map.

Equations

• Cvc.RBMap.mapValM f map = Cvc.RBMap.filterMapValM (fun (x1 : α) (x2 : β) => some <$> f x1 x2) map

def Cvc.RBMap.filterMapVal {α : Type} [Ord α] {β γ : Type} (f : α → β → Option γ) (map : RBMap α β) : RBMap α γ

Filter/map over the values of a map.

Equations

• Cvc.RBMap.filterMapVal f map = Cvc.RBMap.filterMapValM f map

def Cvc.RBMap.filterMapValToArrayM {α : Type} [Ord α] {m : Type u_1 → Type u_2} {β : Type} {γ : Type u_1} [Monad m] (f : α → β → m (Option γ)) (map : RBMap α β) : m (Array γ)

Monadic filter/map over the values of a map into an array of values.

Equations

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

def Cvc.RBMap.filterMapValToArray {α : Type} [Ord α] {β : Type} {γ : Type u_1} (f : α → β → Option γ) (map : RBMap α β) : Array γ

Filter/map over the values of a map into an array of values.

Equations

• Cvc.RBMap.filterMapValToArray f map = Cvc.RBMap.filterMapValToArrayM f map

def Cvc.RBMap.mapValToArrayM {α : Type} [Ord α] {m : Type u_1 → Type u_2} {β : Type} {γ : Type u_1} [Monad m] (f : α → β → m γ) (map : RBMap α β) : m (Array γ)

Monadic map over the values of a map into an array of values.

Equations

• Cvc.RBMap.mapValToArrayM f map = Cvc.RBMap.filterMapValToArrayM (fun (x1 : α) (x2 : β) => some <$> f x1 x2) map

def Cvc.RBMap.mapValToArray {α : Type} [Ord α] {β : Type} {γ : Type u_1} (f : α → β → γ) (map : RBMap α β) : Array γ

Map over the values of a map into an array of values.

Equations

• Cvc.RBMap.mapValToArray f map = Cvc.RBMap.mapValToArrayM f map

def Cvc.RBMap.mapOnlyValM {α : Type} [Ord α] {m : Type → Type u_1} {β γ : Type} [Monad m] (f : β → m γ) (map : RBMap α β) : m (RBMap α γ)

Monadic key-ignoring map over the values of a map.

Equations

• Cvc.RBMap.mapOnlyValM f map = Cvc.RBMap.mapValM (fun (x : α) => f) map

def Cvc.RBMap.mapOnlyVal {α : Type} [Ord α] {β γ : Type} (f : β → γ) (map : RBMap α β) : RBMap α γ

Key-ignoring map over the values of a map.

Equations

• Cvc.RBMap.mapOnlyVal f map = Cvc.RBMap.mapVal (fun (x : α) => f) map

def Cvc.RBMap.filterMapOnlyValM {α : Type} [Ord α] {m : Type → Type u_1} {β γ : Type} [Monad m] (f : β → m (Option γ)) (map : RBMap α β) : m (RBMap α γ)

Key-ignoring monadic filter/map over the values of a map.

Equations

• Cvc.RBMap.filterMapOnlyValM f map = Cvc.RBMap.filterMapValM (fun (x : α) => f) map

def Cvc.RBMap.filterMapOnlyVal {α : Type} [Ord α] {β γ : Type} (f : β → Option γ) (map : RBMap α β) : RBMap α γ

Key-ignoring filter/map over the values of a map.

Equations

• Cvc.RBMap.filterMapOnlyVal f map = Cvc.RBMap.filterMapOnlyValM f map

def Cvc.RBMap.filterMapOnlyValToArrayM {α : Type} [Ord α] {m : Type u_1 → Type u_2} {β : Type} {γ : Type u_1} [Monad m] (f : β → m (Option γ)) (map : RBMap α β) : m (Array γ)

Key-ignoring filter/map over the values of a map into an array of values.

Equations

• Cvc.RBMap.filterMapOnlyValToArrayM f map = Cvc.RBMap.filterMapValToArrayM (fun (x : α) => f) map

def Cvc.RBMap.filterMapOnlyValToArray {α : Type} [Ord α] {β : Type} {γ : Type u_1} (f : β → Option γ) (map : RBMap α β) : Array γ

Key-ignoring filter/map over the values of a map into an array of values.

Equations

• Cvc.RBMap.filterMapOnlyValToArray f map = Cvc.RBMap.filterMapOnlyValToArrayM f map

def Cvc.RBMap.mapOnlyValToArrayM {α : Type} [Ord α] {m : Type u_1 → Type u_2} {β : Type} {γ : Type u_1} [Monad m] (f : β → m γ) (map : RBMap α β) : m (Array γ)

Key-ignoring monadic map over the values of a map into an array of values.

Equations

• Cvc.RBMap.mapOnlyValToArrayM f map = Cvc.RBMap.mapValToArrayM (fun (x : α) => f) map

def Cvc.RBMap.mapOnlyValToArray {α : Type} [Ord α] {β : Type} {γ : Type u_1} (f : β → γ) (map : RBMap α β) : Array γ

Key-ignoring map over the values of a map into an array of values.

Equations

• Cvc.RBMap.mapOnlyValToArray f map = Cvc.RBMap.mapOnlyValToArrayM f map

def Cvc.RBMap.filterMapFoldM {α : Type} [Ord α] {m : Type → Type u_1} {β γ Acc : Type} [Monad m] (init : Acc) (f : Acc → α → β → m (Acc × Option γ)) (map : RBMap α β) : m (Acc × RBMap α γ)

Equations

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

@[reducible, inline]

abbrev Cvc.RBSet (α : Type) [Ord α] : Type

Equations

• Cvc.RBSet α = Batteries.RBSet α compare

def Cvc.RBSet.empty {α : Type} [Ord α] : RBSet α

The empty set.

Equations

• Cvc.RBSet.empty = Batteries.RBSet.empty

def Cvc.RBSet.filter {α : Type} [Ord α] (set : RBSet α) (f : α → Bool) : RBSet α

Removes from set the elements elm for which ¬ f elm.

Equations

• Cvc.RBSet.filter = Batteries.RBSet.filter

def Cvc.RBSet.insert {α : Type} [Ord α] (set : RBSet α) : α → RBSet α

Inserts an element in the set.

See also RBSet.insert'.

Equations

• Cvc.RBSet.insert = Batteries.RBSet.insert

def Cvc.RBSet.insert' {α : Type} [Ord α] (set : RBSet α) (elm : α) : Bool × RBSet α

Inserts an element in the set, yields true iff the element is new.

See also RBSet.insert.

Equations

• set.insert' elm = (Batteries.RBSet.contains set elm, set.insert elm)

def Cvc.RBSet.erase {α : Type} [Ord α] (set : RBSet α) (k : α) : RBSet α

Removes an element from a set.

See also RBSet.erase'.

Equations

• set.erase k = Batteries.RBSet.erase set (compare k)

def Cvc.RBSet.erase' {α : Type} [Ord α] (set : RBSet α) (elm : α) : Bool × RBSet α

Removes an element from a set, yields true iff the element was there.

See also RBSet.erase

Equations

• set.erase' elm = (Batteries.RBSet.contains set elm, set.insert elm)

def Cvc.Decidable.conj {p q : Prop} [Decidable p] [Decidable q] : Decidable (p ∧ q)

Equations

• Cvc.Decidable.conj = inferInstance

def Cvc.Decidable.conj' {p q : Prop} (ip : Decidable p) (iq : Decidable q) : Decidable (p ∧ q)

Equations

• Cvc.Decidable.conj' ip iq = inferInstance

def Cvc.termLs!_ : Lean.ParserDescr

Equations

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

inductive Cvc.CheckSat : Type

A check-sat result.

• sat : CheckSat

  Formulas asserted are satisfiable, i.e. a model exists.

• unsat : CheckSat

  Formulas are unsatisfiable, no assignment of the symbols makes them true.

• unknown (desc : String) : CheckSat

  Solver returned unknown.

• other (desc : String) : CheckSat

  Solver returned some unexpected result.

def Cvc.CheckSat.isSat? : CheckSat → Option Bool

Conversion to a simple is sat? flag, none on unknown/unexpected results.

Equations

• Cvc.CheckSat.sat.isSat? = some true
• Cvc.CheckSat.unsat.isSat? = some false
• (Cvc.CheckSat.unknown desc).isSat? = none
• (Cvc.CheckSat.other desc).isSat? = none

inductive Cvc.Error : Type

• internal (msg : String) : Error
• unsupported (msg : String) : Error
• userError (msg : String) : Error

instance Cvc.instInhabitedError : Inhabited Error

Equations

• Cvc.instInhabitedError = { default := Cvc.Error.internal default }

class Cvc.Error.AsString (α : Type) : Type

Used to allow String and Unit → String as context messages.

• asString : α → String

  Conversion to strings.

instance Cvc.Error.instAsStringString : AsString String

Equations

• Cvc.Error.instAsStringString = { asString := id }

instance Cvc.Error.instAsStringForallUnitString : AsString (Unit → String)

Equations

• Cvc.Error.instAsStringForallUnitString = { asString := fun (f : Unit → String) => f () }

def Cvc.Error.mapMsg (f : String → String) : Error → Error

Equations

• Cvc.Error.mapMsg f (Cvc.Error.internal msg) = Cvc.Error.internal (f msg)
• Cvc.Error.mapMsg f (Cvc.Error.unsupported msg) = Cvc.Error.unsupported (f msg)
• Cvc.Error.mapMsg f (Cvc.Error.userError msg) = Cvc.Error.userError (f msg)

def Cvc.Error.append (self : Error) (txt : String) (newline : Bool := true) : Error

Equations

• self.append txt newline = Cvc.Error.mapMsg (fun (x : String) => x ++ if newline = true then "\n" ++ txt else txt) self

def Cvc.Error.toCvc5 : Error → cvc5.Error

Equations

• (Cvc.Error.internal "a value is missing").toCvc5 = cvc5.Error.missingValue
• (Cvc.Error.internal msg).toCvc5 = cvc5.Error.error msg
• (Cvc.Error.unsupported msg).toCvc5 = cvc5.Error.unsupported msg
• (Cvc.Error.userError msg).toCvc5 = cvc5.Error.error msg

def Cvc.Error.ofCvc5 : cvc5.Error → Error

Equations

• Cvc.Error.ofCvc5 cvc5.Error.missingValue = Cvc.Error.internal "a value is missing"
• Cvc.Error.ofCvc5 (cvc5.Error.error msg) = Cvc.Error.internal (toString "" ++ toString msg ++ toString "")
• Cvc.Error.ofCvc5 (cvc5.Error.option msg) = Cvc.Error.internal (toString "option error: " ++ toString msg ++ toString "")
• Cvc.Error.ofCvc5 (cvc5.Error.unsupported msg) = Cvc.Error.unsupported msg
• Cvc.Error.ofCvc5 (cvc5.Error.recoverable msg) = Cvc.Error.internal (toString "recoverable: " ++ toString msg ++ toString "")

instance Cvc.Error.instMonadLiftExceptError : MonadLift (Except cvc5.Error) (Except Error)

Equations

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

instance Cvc.Error.instCoeError : Coe cvc5.Error Error

Equations

• Cvc.Error.instCoeError = { coe := Cvc.Error.ofCvc5 }

def Cvc.Error.toString : Error → String

Equations

• (Cvc.Error.internal msg).toString = "internal error: " ++ msg
• (Cvc.Error.unsupported msg).toString = "unsupported: " ++ msg
• (Cvc.Error.userError msg).toString = "user error: " ++ msg

instance Cvc.Error.instToString : ToString Error

Equations

• Cvc.Error.instToString = { toString := Cvc.Error.toString }

def Cvc.Error.throwUser {m : Type u_1 → Type u_2} [MonadExcept Error m] (msg : String) {α : Type u_1} : m α

Throws an Error.userError.

Equations

• Cvc.throwUser msg = throw (Cvc.Error.userError msg)

def Cvc.Error.throwInternal {m : Type u_1 → Type u_2} [MonadExcept Error m] (msg : String) {α : Type u_1} : m α

Throws an Error.internal.

Equations

• Cvc.throwInternal msg = throw (Cvc.Error.internal msg)

def Cvc.Error.throwUnreachable {m : Type u_1 → Type u_2} [MonadExcept Error m] {α : Type u_1} (msg : String := "") : m α

Throws an Error.internal about unreachable code.

Equations

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

@[reducible, inline]

abbrev Cvc.ResT (m : Type → Type u_1) (α : Type) : Type u_1

Equations

• Cvc.ResT m = ExceptT Cvc.Error m

@[reducible, inline]

abbrev Cvc.ResIO (α : Type) : Type

Equations

• Cvc.ResIO = Cvc.ResT IO

@[reducible, inline]

abbrev Cvc.Res (α : Type) : Type

Error-result monad.

Equations

• Cvc.Res = Cvc.ResT Id

@[reducible, inline]

abbrev Cvc.Res.ok {α : Type} : α → Res α

A success value of type α

Equations

• Cvc.Res.ok = Except.ok

@[reducible, inline]

abbrev Cvc.Res.error {α : Type} : Error → Res α

A failure value of type ε

Equations

• Cvc.Res.error = Except.error

instance Cvc.Res.instMonadLiftExceptError : MonadLift (Except cvc5.Error) Res

Equations

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

instance Cvc.Res.instMonadLiftExceptError_1 : MonadLift (Except cvc5.Error) Res

Equations

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

instance Cvc.Res.instMonadLiftResTOfMonad {m : Type → Type u_1} [Monad m] : MonadLift Res (ResT m)

Equations

• Cvc.Res.instMonadLiftResTOfMonad = { monadLift := fun {α : Type} => pure }

def Cvc.Res.fail {α : Type} (e : Error) : Res α

Equations

• Cvc.Res.fail e = Cvc.Res.error e

def Cvc.Res.failInternal {α : Type} (e : String) : Res α

Equations

• Cvc.Res.failInternal e = Except.error (Cvc.Error.internal e)

def Cvc.Res.failUser {α : Type} (e : String) : Res α

Equations

• Cvc.Res.failUser e = Except.error (Cvc.Error.userError e)

def Cvc.Res.failTodo {α : Type} (e : String) : Res α

Equations

• Cvc.Res.failTodo e = Except.error (Cvc.Error.unsupported e)

def Cvc.Res.context {S α : Type} [A : Error.AsString S] (s : S) : Res α → Res α

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Res.context s (Except.ok val) = Cvc.Res.ok val

def Cvc.Res.lift {α : Type} : Except cvc5.Error α → Res α

Equations

• Cvc.Res.lift = liftM

Helpers

structure Cvc.ArrayMin (n : Nat) (α : Type u) : Type u

• mk' :: (
• pref : Array α
• inv : self.pref.size = n
• suff : Array α
• )

instance Cvc.instHashableArrayMin {n✝ : Nat} {α✝ : Type u_1} [Hashable α✝] : Hashable (ArrayMin n✝ α✝)

Equations

• Cvc.instHashableArrayMin = { hash := Cvc.hashArrayMin✝ }

instance Cvc.ArrayMin.instInhabited {α : Type u_1} {n : Nat} [Inhabited α] : Inhabited (ArrayMin n α)

Equations

• Cvc.ArrayMin.instInhabited = { default := { pref := Array.replicate n default, inv := ⋯ } }

def Cvc.ArrayMin.mk {α : Type u_1} (pref : Array α) (suff : Array α := #[]) : ArrayMin pref.size α

Equations

• Cvc.ArrayMin.mk pref suff = { pref := pref, inv := ⋯, suff := suff }

def Cvc.ArrayMin.toString {α : Type u_1} {n : Nat} [ToString α] (self : ArrayMin n α) : String

Equations

• self.toString = if self.suff.isEmpty = true then toString self.pref else toString "" ++ toString self.pref ++ toString "" ++ toString self.suff ++ toString ""

instance Cvc.ArrayMin.instToString {α : Type u_1} {n : Nat} [ToString α] : ToString (ArrayMin n α)

Equations

• Cvc.ArrayMin.instToString = { toString := Cvc.ArrayMin.toString }

@[simp]

theorem Cvc.ArrayMin.pref_size {n : Nat} {α : Type u_1} (self : ArrayMin n α) : self.pref.size = n

@[reducible, inline]

abbrev Cvc.ArrayMin.size {n : Nat} {α : Type u_1} (self : ArrayMin n α) : Nat

Equations

• self.size = n + self.suff.size

@[simp]

theorem Cvc.ArrayMin.min_le_size {n : Nat} {α : Type u_1} (self : ArrayMin n α) : n ≤ self.size

def Cvc.ArrayMin.get {n : Nat} {α : Type u_1} (self : ArrayMin n α) (i : Fin self.size) : α

Equations

• self.get ⟨i, h_i⟩ = if h : i < n then have this := ⋯; self.pref[i] else have this := ⋯; self.suff[i - n]

instance Cvc.ArrayMin.instGetElem {n : Nat} {α : Type u_1} : GetElem (ArrayMin n α) Nat α fun (arr : ArrayMin n α) (i : Nat) => i < arr.size

Equations

• Cvc.ArrayMin.instGetElem = { getElem := fun (self : Cvc.ArrayMin n α) (i : Nat) (h_i : i < self.size) => self.get ⟨i, h_i⟩ }

def Cvc.ArrayMin.get? {n : Nat} {α : Type u_1} (self : ArrayMin n α) (i : Nat) : Option α

Equations

• self.get? i = if h : i < self.size then some (self.get ⟨i, h⟩) else none

def Cvc.ArrayMin.get! {n : Nat} {α : Type u_1} [Inhabited α] (self : ArrayMin n α) (i : Nat) : α

Equations

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

def Cvc.ArrayMin.getN {n : Nat} {α : Type u_1} (self : ArrayMin n α) (i : Nat) (h : i < n := by decide) : α

Equations

• self.getN i h = self.pref[i]

def Cvc.ArrayMin.toArray {n : Nat} {α : Type u_1} (self : ArrayMin n α) : Array α

Equations

• self.toArray = self.pref ++ self.suff

def Cvc.ArrayMin.toList {n : Nat} {α : Type u_1} (self : ArrayMin n α) : List α

Equations

• self.toList = self.pref.toList ++ self.suff.toList

def Cvc.ArrayMin.push {n : Nat} {α : Type u_1} (self : ArrayMin n α) (a : α) : ArrayMin n α

Equations

• self.push a = { pref := self.pref, inv := ⋯, suff := self.suff.push a }

def Cvc.ArrayMin.drainFirst {n : Nat} {α : Type u_1} : ArrayMin n.succ α → α × ArrayMin n α

Equations

• { pref := { toList := fst :: pref }, inv := h_pref', suff := suff }.drainFirst = (fst, { pref := { toList := pref }, inv := ⋯, suff := suff })

instance Cvc.ArrayMin.instForIn {n : Nat} {α : Type u_1} {m : Type u_2 → Type u_3} : ForIn m (ArrayMin n α) α

Equations

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

structure Cvc.ArrayMin.Frame (n : Nat) (α : Type u) : Type u

• pref : Array α
• suff : Array α

instance Cvc.ArrayMin.instInhabitedFrame {a✝ : Nat} {a✝¹ : Type u_1} : Inhabited (Frame a✝ a✝¹)

Equations

• Cvc.ArrayMin.instInhabitedFrame = { default := { pref := default, suff := default } }

def Cvc.ArrayMin.Frame.new {α : Type u_1} (n : Nat) : Frame n α

Equations

• Cvc.ArrayMin.Frame.new n = { }

def Cvc.ArrayMin.Frame.push {n : Nat} {α : Type u_1} (self : Frame n α) (a : α) : Frame n α

Equations

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

def Cvc.ArrayMin.Frame.finalize {n : Nat} {α : Type u_1} (self : Frame n α) [Inhabited α] : ArrayMin n α

Equations

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

def Cvc.ArrayMin.newFrame {n : Nat} {α : Type u_1} {β : Type u_2} : ArrayMin n α → Frame n β

Equations

• x✝.newFrame = Cvc.ArrayMin.Frame.new n

structure Cvc.ArrayMin.Iter (n : Nat) (α : Type u) : Type u

• val : ArrayMin n α
• pos : Nat

@[reducible, inline]

abbrev Cvc.ArrayMin.Iter.isNotDone {n : Nat} {α : Type u_1} (self : Iter n α) : Bool

Equations

• self.isNotDone = decide (self.pos < self.val.size)

@[reducible, inline]

abbrev Cvc.ArrayMin.Iter.isDone {n : Nat} {α : Type u_1} (self : Iter n α) : Bool

Equations

• self.isDone = decide ¬self.isNotDone = true

def Cvc.ArrayMin.Iter.next? {n : Nat} {α : Type u_1} (self : Iter n α) : Option α × Iter n α

Equations

• self.next? = if h : self.isNotDone = true then let next := self.val.get ⟨self.pos, ⋯⟩; (some next, { val := self.val, pos := self.pos.succ }) else (none, self)

def Cvc.ArrayMin.iter {n : Nat} {α : Type u_1} (self : ArrayMin n α) : Iter n α

Equations

• self.iter = { val := self, pos := 0 }