Comparse.Formats.Derived

source

def Comparse.NonExtensibleMessageFormat.isomorphic {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) :

NonExtensibleMessageFormat Bytes b

Equations

mf.isomorphic f g = mf.subsetIsomorphic (fun (x : a) => some (f x)) g

Instances For

source

class Comparse.LeftInverse {b : Sort u_1} {a : Sort u_2} (g : b → a) (f : a → b) :

Prop

left_inv : Function.LeftInverse g f

Instances

source

class Comparse.RightInverse {b : Sort u_1} {a : Sort u_2} (g : b → a) (f : a → b) :

Prop

right_inv : Function.RightInverse g f

Instances

source

instance Comparse.NonExtensibleMessageFormat.isomorphic.instIsNonAmbiguousOfRightInverse {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) [mf.IsNonAmbiguous] [RightInverse g f] :

(mf.isomorphic f g).IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.isomorphic.instHasUniqueRepresentationOfLeftInverse {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) [mf.HasUniqueRepresentation] [LeftInverse g f] :

(mf.isomorphic f g).HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.isomorphic.instParseConsumes {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) [mf.ParseConsumes] :

(mf.isomorphic f g).ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.isomorphic.wf_eq {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : b) :

(mf.isomorphic f g).wf pred x = mf.wf pred (g x)

source

def Comparse.NonExtensibleMessageFormat.triviallyIsomorphic {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) :

autoParam (Function.LeftInverse g f) triviallyIsomorphic._auto_1 → autoParam (Function.RightInverse g f) triviallyIsomorphic._auto_3 → NonExtensibleMessageFormat Bytes b

Equations

mf.triviallyIsomorphic f g x✝¹ x✝ = mf.isomorphic f g

Instances For

source

instance Comparse.NonExtensibleMessageFormat.triviallyIsomorphic.instIsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (h_left : Function.LeftInverse g f) (h_right : Function.RightInverse g f) [mf.IsNonAmbiguous] :

(mf.triviallyIsomorphic f g h_left h_right).IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.triviallyIsomorphic.instHasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (h_left : Function.LeftInverse g f) (h_right : Function.RightInverse g f) [mf.HasUniqueRepresentation] :

(mf.triviallyIsomorphic f g h_left h_right).HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.triviallyIsomorphic.instParseConsumes {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (h_left : Function.LeftInverse g f) (h_right : Function.RightInverse g f) [mf.ParseConsumes] :

(mf.triviallyIsomorphic f g h_left h_right).ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.triviallyIsomorphic.wf_eq {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (h_left : Function.LeftInverse g f) (h_right : Function.RightInverse g f) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : b) :

(mf.triviallyIsomorphic f g h_left h_right).wf pred x = mf.wf pred (g x)

source

def Comparse.ExtensibleMessageFormat.isomorphic {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) :

ExtensibleMessageFormat Bytes b

Equations

mf.isomorphic f g = mf.subsetIsomorphic (fun (x : a) => some (f x)) g

Instances For

source

instance Comparse.ExtensibleMessageFormat.isomorphic.instIsNonAmbiguousOfRightInverse {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) [mf.IsNonAmbiguous] [RightInverse g f] :

(mf.isomorphic f g).IsNonAmbiguous

source

instance Comparse.ExtensibleMessageFormat.isomorphic.instHasUniqueRepresentationOfLeftInverse {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) [mf.HasUniqueRepresentation] [LeftInverse g f] :

(mf.isomorphic f g).HasUniqueRepresentation

source

@[simp]

theorem Comparse.ExtensibleMessageFormat.isomorphic.wf_eq {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : b) :

(mf.isomorphic f g).wf pred x = mf.wf pred (g x)

source

def Comparse.ExtensibleMessageFormat.triviallyIsomorphic {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) :

autoParam (Function.LeftInverse g f) triviallyIsomorphic._auto_1 → autoParam (Function.RightInverse g f) triviallyIsomorphic._auto_3 → ExtensibleMessageFormat Bytes b

Equations

mf.triviallyIsomorphic f g x✝¹ x✝ = mf.isomorphic f g

Instances For

source

instance Comparse.ExtensibleMessageFormat.triviallyIsomorphic.instIsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (h_left : Function.LeftInverse g f) (h_right : Function.RightInverse g f) [mf.IsNonAmbiguous] :

(mf.triviallyIsomorphic f g h_left h_right).IsNonAmbiguous

source

instance Comparse.ExtensibleMessageFormat.triviallyIsomorphic.instHasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (h_left : Function.LeftInverse g f) (h_right : Function.RightInverse g f) [mf.HasUniqueRepresentation] :

(mf.triviallyIsomorphic f g h_left h_right).HasUniqueRepresentation

source

@[simp]

theorem Comparse.ExtensibleMessageFormat.triviallyIsomorphic.wf_eq {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → b) (g : b → a) (h_left : Function.LeftInverse g f) (h_right : Function.RightInverse g f) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : b) :

(mf.triviallyIsomorphic f g h_left h_right).wf pred x = mf.wf pred (g x)

source

def Comparse.NonExtensibleMessageFormat.subtype {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] :

NonExtensibleMessageFormat Bytes (Subtype p)

Equations

mf.subtype p = mf.subsetIsomorphic Comparse.NonExtensibleMessageFormat.subtype.f✝ Comparse.NonExtensibleMessageFormat.subtype.g✝

Instances For

source

instance Comparse.NonExtensibleMessageFormat.subtype.instIsNonAmbiguousSubtype {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] [mf.IsNonAmbiguous] :

(mf.subtype p).IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.subtype.instHasUniqueRepresentationSubtype {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] [mf.HasUniqueRepresentation] :

(mf.subtype p).HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.subtype.instParseConsumesSubtype {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] [mf.ParseConsumes] :

(mf.subtype p).ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.subtype.wf_eq {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : Subtype p) :

(mf.subtype p).wf pred x = mf.wf pred x.val

source

def Comparse.ExtensibleMessageFormat.subtype {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] :

ExtensibleMessageFormat Bytes (Subtype p)

Equations

mf.subtype p = mf.subsetIsomorphic Comparse.ExtensibleMessageFormat.subtype.f✝ Comparse.ExtensibleMessageFormat.subtype.g✝

Instances For

source

instance Comparse.ExtensibleMessageFormat.subtype.instIsNonAmbiguousSubtype {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] [mf.IsNonAmbiguous] :

(mf.subtype p).IsNonAmbiguous

source

instance Comparse.ExtensibleMessageFormat.subtype.instHasUniqueRepresentationSubtype {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] [mf.HasUniqueRepresentation] :

(mf.subtype p).HasUniqueRepresentation

source

@[simp]

theorem Comparse.ExtensibleMessageFormat.subtype.wf_eq {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (p : a → Prop) [DecidablePred p] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : Subtype p) :

(mf.subtype p).wf pred x = mf.wf pred x.val

source

def Comparse.NonExtensibleMessageFormat.prod {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : NonExtensibleMessageFormat Bytes b) :

NonExtensibleMessageFormat Bytes (a × b)

Equations

mfa.prod mfb = (mfa.sigma fun (x : a) => mfb).isomorphic Comparse.NonExtensibleMessageFormat.prod.f✝ Comparse.NonExtensibleMessageFormat.prod.g✝

Instances For

source

instance Comparse.NonExtensibleMessageFormat.prod.instIsNonAmbiguousProd {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : NonExtensibleMessageFormat Bytes b) [mfa.IsNonAmbiguous] [mfb.IsNonAmbiguous] :

(mfa.prod mfb).IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.prod.instHasUniqueRepresentationProd {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : NonExtensibleMessageFormat Bytes b) [mfa.HasUniqueRepresentation] [mfb.HasUniqueRepresentation] :

(mfa.prod mfb).HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.prod.instParseConsumesProd {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : NonExtensibleMessageFormat Bytes b) [mfa.ParseConsumes] :

(mfa.prod mfb).ParseConsumes

source

instance Comparse.NonExtensibleMessageFormat.prod.instParseConsumesProd_1 {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : NonExtensibleMessageFormat Bytes b) [mfb.ParseConsumes] :

(mfa.prod mfb).ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.prod.wf_eq {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : NonExtensibleMessageFormat Bytes b) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : a × b) :

(mfa.prod mfb).wf pred x = (mfa.wf pred x.fst ∧ mfb.wf pred x.snd)

source

def Comparse.ExtensibleMessageFormat.prod {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : ExtensibleMessageFormat Bytes b) :

ExtensibleMessageFormat Bytes (a × b)

Equations

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

Instances For

source

instance Comparse.ExtensibleMessageFormat.prod.instIsNonAmbiguousProdOfIsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : ExtensibleMessageFormat Bytes b) [mfa.IsNonAmbiguous] [mfb.IsNonAmbiguous] :

(prod mfa mfb).IsNonAmbiguous

source

instance Comparse.ExtensibleMessageFormat.prod.instHasUniqueRepresentationProdOfHasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : ExtensibleMessageFormat Bytes b) [mfa.HasUniqueRepresentation] [mfb.HasUniqueRepresentation] :

(prod mfa mfb).HasUniqueRepresentation

source

@[simp]

theorem Comparse.ExtensibleMessageFormat.prod.wf_eq {Bytes : Type} [BytesLike Bytes] {a b : Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : ExtensibleMessageFormat Bytes b) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : a × b) :

(prod mfa mfb).wf pred x = (mfa.wf pred x.fst ∧ mfb.wf pred x.snd)

source

def Comparse.ExtensibleMessageFormat.byteArray {Bytes : Type} [BytesLike Bytes] :

ExtensibleMessageFormat Bytes ByteArray

Equations

Comparse.ExtensibleMessageFormat.byteArray = Comparse.ExtensibleMessageFormat.bytes.subsetIsomorphic Comparse.BytesLike.toByteArray Comparse.BytesLike.fromByteArray

Instances For

source

instance Comparse.ExtensibleMessageFormat.instIsNonAmbiguousByteArrayByteArray {Bytes : Type} [BytesLike Bytes] :

byteArray.IsNonAmbiguous

source

instance Comparse.ExtensibleMessageFormat.instHasUniqueRepresentationByteArrayByteArray {Bytes : Type} [BytesLike Bytes] :

byteArray.HasUniqueRepresentation

source

@[simp]

theorem Comparse.ExtensibleMessageFormat.byteArray.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : ByteArray) :

byteArray.wf pred x

source

def Comparse.ExtensibleMessageFormat.string {Bytes : Type} [BytesLike Bytes] :

ExtensibleMessageFormat Bytes String

Equations

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

Instances For

source

instance Comparse.ExtensibleMessageFormat.instIsNonAmbiguousStringString {Bytes : Type} [BytesLike Bytes] :

string.IsNonAmbiguous

source

instance Comparse.ExtensibleMessageFormat.instHasUniqueRepresentationStringString {Bytes : Type} [BytesLike Bytes] :

string.HasUniqueRepresentation

source

@[simp]

theorem Comparse.ExtensibleMessageFormat.string.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : String) :

string.wf pred x

source

def Comparse.NonExtensibleMessageFormat.fixedLengthBytes {Bytes : Type} [BytesLike Bytes] (len : Nat) :

NonExtensibleMessageFormat Bytes { b : Bytes // BytesLike.length b = len }

Equations

Comparse.NonExtensibleMessageFormat.fixedLengthBytes len = (Comparse.ExtensibleMessageFormat.bytes.subtype fun (b : Bytes) => Comparse.BytesLike.length b = len).toNonExtensible len ⋯

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousSubtypeEqNatLengthFixedLengthBytes {Bytes : Type} [BytesLike Bytes] (len : Nat) :

(fixedLengthBytes len).IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationSubtypeEqNatLengthFixedLengthBytes {Bytes : Type} [BytesLike Bytes] (len : Nat) :

(fixedLengthBytes len).HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.fixedLengthBytes.instParseConsumesSubtypeEqNatLengthOfNeZero {Bytes : Type} [BytesLike Bytes] (len : Nat) [NeZero len] :

(fixedLengthBytes len).ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.fixedLengthBytes.wf_eq {Bytes : Type} [BytesLike Bytes] (len : Nat) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : { b : Bytes // BytesLike.length b = len }) :

(fixedLengthBytes len).wf pred x = pred x.val

source

def Comparse.NonExtensibleMessageFormat.fixedLengthByteArray {Bytes : Type} [BytesLike Bytes] (len : Nat) :

NonExtensibleMessageFormat Bytes { b : ByteArray // b.size = len }

Equations

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

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousSubtypeByteArrayEqNatSizeFixedLengthByteArray {Bytes : Type} [BytesLike Bytes] (len : Nat) :

(fixedLengthByteArray len).IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationSubtypeByteArrayEqNatSizeFixedLengthByteArray {Bytes : Type} [BytesLike Bytes] (len : Nat) :

(fixedLengthByteArray len).HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.fixedLengthByteArray.instParseConsumesSubtypeByteArrayEqNatSizeOfNeZero {Bytes : Type} [BytesLike Bytes] (len : Nat) [NeZero len] :

(fixedLengthByteArray len).ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.fixedLengthByteArray.wf_eq {Bytes : Type} [BytesLike Bytes] (len : Nat) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : { b : ByteArray // b.size = len }) :

(fixedLengthByteArray len).wf pred x

source

def Comparse.NonExtensibleMessageFormat.bitVec {Bytes : Type} [BytesLike Bytes] (w : Nat) :

NonExtensibleMessageFormat Bytes (BitVec (8 * w))

Equations

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

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousBitVecHMulNatOfNatBitVec {Bytes : Type} [BytesLike Bytes] (w : Nat) :

(bitVec w).IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationBitVecHMulNatOfNatBitVec {Bytes : Type} [BytesLike Bytes] (w : Nat) :

(bitVec w).HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.bitVec.instParseConsumesBitVecHMulNatOfNatOfNeZero {Bytes : Type} [BytesLike Bytes] (w : Nat) [NeZero w] :

(bitVec w).ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.bitVec.wf_eq {Bytes : Type} [BytesLike Bytes] (w : Nat) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : BitVec (8 * w)) :

(bitVec w).wf pred x

source

def Comparse.NonExtensibleMessageFormat.uint8 {Bytes : Type} [BytesLike Bytes] :

NonExtensibleMessageFormat Bytes UInt8

Equations

Comparse.NonExtensibleMessageFormat.uint8 = (Comparse.NonExtensibleMessageFormat.bitVec 1).isomorphic UInt8.ofBitVec UInt8.toBitVec

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousUInt8Uint8 {Bytes : Type} [BytesLike Bytes] :

uint8.IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationUInt8Uint8 {Bytes : Type} [BytesLike Bytes] :

uint8.HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesUInt8Uint8 {Bytes : Type} [BytesLike Bytes] :

uint8.ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.uint8.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : UInt8) :

uint8.wf pred x

source

def Comparse.NonExtensibleMessageFormat.uint16 {Bytes : Type} [BytesLike Bytes] :

NonExtensibleMessageFormat Bytes UInt16

Equations

Comparse.NonExtensibleMessageFormat.uint16 = (Comparse.NonExtensibleMessageFormat.bitVec 2).isomorphic UInt16.ofBitVec UInt16.toBitVec

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousUInt16Uint16 {Bytes : Type} [BytesLike Bytes] :

uint16.IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationUInt16Uint16 {Bytes : Type} [BytesLike Bytes] :

uint16.HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesUInt16Uint16 {Bytes : Type} [BytesLike Bytes] :

uint16.ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.uint16.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : UInt16) :

uint16.wf pred x

source

def Comparse.NonExtensibleMessageFormat.uint32 {Bytes : Type} [BytesLike Bytes] :

NonExtensibleMessageFormat Bytes UInt32

Equations

Comparse.NonExtensibleMessageFormat.uint32 = (Comparse.NonExtensibleMessageFormat.bitVec 4).isomorphic UInt32.ofBitVec UInt32.toBitVec

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousUInt32Uint32 {Bytes : Type} [BytesLike Bytes] :

uint32.IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationUInt32Uint32 {Bytes : Type} [BytesLike Bytes] :

uint32.HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesUInt32Uint32 {Bytes : Type} [BytesLike Bytes] :

uint32.ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.uint32.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : UInt32) :

uint32.wf pred x

source

def Comparse.NonExtensibleMessageFormat.uint64 {Bytes : Type} [BytesLike Bytes] :

NonExtensibleMessageFormat Bytes UInt64

Equations

Comparse.NonExtensibleMessageFormat.uint64 = (Comparse.NonExtensibleMessageFormat.bitVec 8).isomorphic UInt64.ofBitVec UInt64.toBitVec

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousUInt64Uint64 {Bytes : Type} [BytesLike Bytes] :

uint64.IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationUInt64Uint64 {Bytes : Type} [BytesLike Bytes] :

uint64.HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesUInt64Uint64 {Bytes : Type} [BytesLike Bytes] :

uint64.ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.uint64.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : UInt64) :

uint64.wf pred x

source

def Comparse.NonExtensibleMessageFormat.fin8 {Bytes : Type} [BytesLike Bytes] (n : Nat) (h : n ≤ 256) :

NonExtensibleMessageFormat Bytes (Fin n)

Equations

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

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousFinFin8 {Bytes : Type} [BytesLike Bytes] (n : Nat) (h : n ≤ 256) :

(fin8 n h).IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationFinFin8 {Bytes : Type} [BytesLike Bytes] (n : Nat) (h : n ≤ 256) :

(fin8 n h).HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesFinFin8 {Bytes : Type} [BytesLike Bytes] (n : Nat) (h : n ≤ 256) :

(fin8 n h).ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.fin8.wf_eq {Bytes : Type} [BytesLike Bytes] (n : Nat) (h : n ≤ 256) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : Fin n) :

(fin8 n h).wf pred x

source

def Comparse.NonExtensibleMessageFormat.bool {Bytes : Type} [BytesLike Bytes] :

NonExtensibleMessageFormat Bytes Bool

Equations

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

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousBoolBool {Bytes : Type} [BytesLike Bytes] :

bool.IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationBoolBool {Bytes : Type} [BytesLike Bytes] :

bool.HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesBoolBool {Bytes : Type} [BytesLike Bytes] :

bool.ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.bool.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : Bool) :

bool.wf pred x

source

def Comparse.NonExtensibleMessageFormat.slowNat {Bytes : Type} [BytesLike Bytes] :

NonExtensibleMessageFormat Bytes Nat

Equations

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

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousNatSlowNat {Bytes : Type} [BytesLike Bytes] :

slowNat.IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationNatSlowNat {Bytes : Type} [BytesLike Bytes] :

slowNat.HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesNatSlowNat {Bytes : Type} [BytesLike Bytes] :

slowNat.ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.slowNat.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : Nat) :

slowNat.wf pred x

source

def Comparse.NonExtensibleMessageFormat.slowBytes {Bytes : Type} [BytesLike Bytes] :

NonExtensibleMessageFormat Bytes Bytes

Equations

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

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousSlowBytes {Bytes : Type} [BytesLike Bytes] :

slowBytes.IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationSlowBytes {Bytes : Type} [BytesLike Bytes] :

slowBytes.HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesSlowBytes {Bytes : Type} [BytesLike Bytes] :

slowBytes.ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.slowBytes.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : Bytes) :

slowBytes.wf pred x = pred x

source

def Comparse.NonExtensibleMessageFormat.slowString {Bytes : Type} [BytesLike Bytes] :

NonExtensibleMessageFormat Bytes String

Equations

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

Instances For

source

instance Comparse.NonExtensibleMessageFormat.instIsNonAmbiguousStringSlowString {Bytes : Type} [BytesLike Bytes] :

slowString.IsNonAmbiguous

source

instance Comparse.NonExtensibleMessageFormat.instHasUniqueRepresentationStringSlowString {Bytes : Type} [BytesLike Bytes] :

slowString.HasUniqueRepresentation

source

instance Comparse.NonExtensibleMessageFormat.instParseConsumesStringSlowString {Bytes : Type} [BytesLike Bytes] :

slowString.ParseConsumes

source

@[simp]

theorem Comparse.NonExtensibleMessageFormat.slowString.wf_eq {Bytes : Type} [BytesLike Bytes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : String) :

slowString.wf pred x