instance instDecidableEqForallForallNatBitStreamEval (t₁ : Term) (t₂ : Term) : Decidable (t₁.eval = t₂.eval)

Equations

• instDecidableEqForallForallNatBitStreamEval t₁ t₂ = decidable_of_iff (decideIfZeros (termEvalEqFSM (t₁.xor t₂)).toFSM = true) ⋯

def run_decide (t₁ : Term) (t₂ : Term) : IO Bool

Equations

• run_decide t₁ t₂ = pure (Decidable.decide (t₁.eval = t₂.eval))

def decide (t₁ : Term) (t₂ : Term) : IO Bool

Equations

• _root_.decide t₁ t₂ = run_decide t₁ t₂

def x : Term

Equations

• x = Term.var 0

def y : Term

Equations

• y = Term.var 1

def z : Term

Equations

• z = Term.var 2