Documentation

Init.Data.SInt.Decidable

source
def commandDeclare_decidable_int_quantifiers__ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    instance Int8.instDecidableExists (P : Int8 → Prop) [DecidablePred P] :
    Decidable (∃ (x : Int8), P x)
    Equations
    source
    theorem Int8.forall_iff_forall_ofBitVec {P : Int8 → Prop} :
    (∀ (x : Int8), P x) ↔ ∀ (x : BitVec 8), P (ofBitVec x)
    source
    theorem Int8.exists_iff_exists_ofBitVec {P : Int8 → Prop} :
    (∃ (x : Int8), P x) ↔ ∃ (x : BitVec 8), P (ofBitVec x)
    source
    @[instance_reducible]
    instance Int8.instDecidableForall (P : Int8 → Prop) [DecidablePred P] :
    Decidable (∀ (x : Int8), P x)
    Equations
    source
    theorem Int16.forall_iff_forall_ofBitVec {P : Int16 → Prop} :
    (∀ (x : Int16), P x) ↔ ∀ (x : BitVec 16), P (ofBitVec x)
    source
    theorem Int16.exists_iff_exists_ofBitVec {P : Int16 → Prop} :
    (∃ (x : Int16), P x) ↔ ∃ (x : BitVec 16), P (ofBitVec x)
    source
    @[instance_reducible]
    instance Int16.instDecidableForall (P : Int16 → Prop) [DecidablePred P] :
    Decidable (∀ (x : Int16), P x)
    Equations
    source
    @[instance_reducible]
    instance Int16.instDecidableExists (P : Int16 → Prop) [DecidablePred P] :
    Decidable (∃ (x : Int16), P x)
    Equations
    source
    theorem Int32.forall_iff_forall_ofBitVec {P : Int32 → Prop} :
    (∀ (x : Int32), P x) ↔ ∀ (x : BitVec 32), P (ofBitVec x)
    source
    theorem Int32.exists_iff_exists_ofBitVec {P : Int32 → Prop} :
    (∃ (x : Int32), P x) ↔ ∃ (x : BitVec 32), P (ofBitVec x)
    source
    @[instance_reducible]
    instance Int32.instDecidableExists (P : Int32 → Prop) [DecidablePred P] :
    Decidable (∃ (x : Int32), P x)
    Equations
    source
    @[instance_reducible]
    instance Int32.instDecidableForall (P : Int32 → Prop) [DecidablePred P] :
    Decidable (∀ (x : Int32), P x)
    Equations
    source
    @[instance_reducible]
    instance Int64.instDecidableExists (P : Int64 → Prop) [DecidablePred P] :
    Decidable (∃ (x : Int64), P x)
    Equations
    source
    theorem Int64.exists_iff_exists_ofBitVec {P : Int64 → Prop} :
    (∃ (x : Int64), P x) ↔ ∃ (x : BitVec 64), P (ofBitVec x)
    source
    theorem Int64.forall_iff_forall_ofBitVec {P : Int64 → Prop} :
    (∀ (x : Int64), P x) ↔ ∀ (x : BitVec 64), P (ofBitVec x)
    source
    @[instance_reducible]
    instance Int64.instDecidableForall (P : Int64 → Prop) [DecidablePred P] :
    Decidable (∀ (x : Int64), P x)
    Equations