Equations
Instances For
def
Std.Sat.AIG.RefVec.emptyWithCapacity
{α : Type}
[Hashable α]
[DecidableEq α]
{aig : AIG α}
(c : Nat)
:
aig.RefVec 0
Equations
Instances For
@[simp]
theorem
Std.Sat.AIG.RefVec.emptyWithCapacity_eq
{α : Type}
[Hashable α]
[DecidableEq α]
{aig : AIG α}
{c : Nat}
:
@[inline]
def
Std.Sat.AIG.RefVec.cast'
{α : Type}
[Hashable α]
[DecidableEq α]
{len : Nat}
{aig1 aig2 : AIG α}
(s : aig1.RefVec len)
(h :
(∀ {i : Nat} (h : i < len), s.refs[i].gate < aig1.decls.size) →
∀ {i : Nat} (h : i < len), s.refs[i].gate < aig2.decls.size)
:
aig2.RefVec len
Equations
Instances For
def
Std.Sat.AIG.RefVec.countKnown
{α : Type}
[Hashable α]
[DecidableEq α]
{len : Nat}
(aig : AIG α)
(s : aig.RefVec len)
:
Equations
Instances For
@[irreducible]
def
Std.Sat.AIG.RefVec.countKnown.go
{α : Type}
[Hashable α]
[DecidableEq α]
{len : Nat}
(aig : AIG α)
(s : aig.RefVec len)
(idx acc : Nat)
:
Equations
Instances For
structure
Std.Sat.AIG.BinaryRefVec
{α : Type}
[Hashable α]
[DecidableEq α]
(aig : AIG α)
(len : Nat)
:
Instances For
@[inline]
def
Std.Sat.AIG.BinaryRefVec.cast
{α : Type}
[Hashable α]
[DecidableEq α]
{len : Nat}
{aig1 aig2 : AIG α}
(s : aig1.BinaryRefVec len)
(h : aig1.decls.size ≤ aig2.decls.size)
:
aig2.BinaryRefVec len
Equations
Instances For
@[simp]
@[simp]