def BitVec.«term_≤ᵤ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_≤ᵤ_» = Lean.ParserDescr.trailingNode `BitVec.«term_≤ᵤ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ᵤ ") (Lean.ParserDescr.cat `term 0))

def BitVec.«term_<ᵤ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_<ᵤ_» = Lean.ParserDescr.trailingNode `BitVec.«term_<ᵤ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ᵤ ") (Lean.ParserDescr.cat `term 0))

def BitVec.«term_≥ᵤ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_≥ᵤ_» = Lean.ParserDescr.trailingNode `BitVec.«term_≥ᵤ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≥ᵤ ") (Lean.ParserDescr.cat `term 0))

def BitVec.«term_>ᵤ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_>ᵤ_» = Lean.ParserDescr.trailingNode `BitVec.«term_>ᵤ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >ᵤ ") (Lean.ParserDescr.cat `term 0))

def BitVec.«term_≤ₛ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_≤ₛ_» = Lean.ParserDescr.trailingNode `BitVec.«term_≤ₛ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₛ ") (Lean.ParserDescr.cat `term 0))

def BitVec.«term_<ₛ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_<ₛ_» = Lean.ParserDescr.trailingNode `BitVec.«term_<ₛ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ₛ ") (Lean.ParserDescr.cat `term 0))

def BitVec.«term_≥ₛ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_≥ₛ_» = Lean.ParserDescr.trailingNode `BitVec.«term_≥ₛ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≥ₛ ") (Lean.ParserDescr.cat `term 0))

def BitVec.«term_>ₛ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_>ₛ_» = Lean.ParserDescr.trailingNode `BitVec.«term_>ₛ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >ₛ ") (Lean.ParserDescr.cat `term 0))

instance BitVec.instShiftLeft_sSA {n : Nat} : ShiftLeft (BitVec n)

Equations

• BitVec.instShiftLeft_sSA = { shiftLeft := fun (x y : BitVec n) => x <<< y.toNat }

instance BitVec.instShiftRight_sSA {n : Nat} : ShiftRight (BitVec n)

Equations

• BitVec.instShiftRight_sSA = { shiftRight := fun (x y : BitVec n) => x >>> y.toNat }

def BitVec.«term_>>>ₛ_» : Lean.TrailingParserDescr

Equations

• BitVec.«term_>>>ₛ_» = Lean.ParserDescr.trailingNode `BitVec.«term_>>>ₛ_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol ">>>ₛ") (Lean.ParserDescr.cat `term 76))

inductive BitVec.Refinement {α : Type u} : Option α → Option α → Prop

• bothSome: ∀ {α : Type u} {x y : α}, x = y → some x ⊑ some y
• noneAny: ∀ {α : Type u} {x? : Option α}, none ⊑ x?

def BitVec.Refinement.«term_⊑_» : Lean.TrailingParserDescr

Equations

• BitVec.Refinement.«term_⊑_» = Lean.ParserDescr.trailingNode `BitVec.Refinement.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem BitVec.Refinement.some_some {α : Type u} {x : α} {y : α} : some x ⊑ some y ↔ x = y

@[simp]

theorem BitVec.Refinement.none_left : ∀ {α : Type u_1} {x? : Option α}, none ⊑ x?

theorem BitVec.Refinement.none_right {α : Type u_1} {x? : Option α} : x? ⊑ none ↔ x? = none

theorem BitVec.Refinement.some_left {α : Type u_1} {x : α} {y? : Option α} : some x ⊑ y? ↔ y? = some x

@[simp]

theorem BitVec.Refinement.refl {α : Type u} (x : Option α) : x ⊑ x

theorem BitVec.Refinement.trans {α : Type u} (x : Option α) (y : Option α) (z : Option α) : x ⊑ y → y ⊑ z → x ⊑ z

instance BitVec.Refinement.instDecidableRelOptionOfDecidableEq {α : Type u} [DEQ : DecidableEq α] : DecidableRel BitVec.Refinement

Equations

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

instance BitVec.instCoeBoolOfNatNat_sSA : Coe Bool (BitVec 1)

Equations

• BitVec.instCoeBoolOfNatNat_sSA = { coe := BitVec.ofBool }

def BitVec.coeWidth {m : Nat} {n : Nat} : BitVec m → BitVec n

Equations

• x.coeWidth = BitVec.ofNat n x.toNat

instance BitVec.decPropToBitvec1 (p : Prop) [Decidable p] : CoeDep Prop p (BitVec 1)

Equations

• BitVec.decPropToBitvec1 p = { coe := BitVec.ofBool (decide p) }

theorem BitVec.Int.natCast_pred_of_pos (x : Nat) (h : 0 < x) : ↑x - 1 = ↑(x - 1)