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

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

• left_inv : Function.LeftInverse g f

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

• right_inv : Function.RightInverse g f

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

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

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

@[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)

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

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

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

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

@[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)

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

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

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

@[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)

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

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

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

@[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)

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✝

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

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

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

@[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

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✝

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

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

@[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

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✝

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

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

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

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

@[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)

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.

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

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

@[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)

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

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

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

@[simp]

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

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

Equations

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

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

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

@[simp]

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

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 ⋯

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

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

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

@[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

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.

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

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

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

@[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

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.

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

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

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

@[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

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

Equations

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

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

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

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

@[simp]

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

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

Equations

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

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

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

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

@[simp]

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

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

Equations

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

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

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

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

@[simp]

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

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

Equations

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

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

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

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

@[simp]

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

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.

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

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

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

@[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

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

Equations

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

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

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

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

@[simp]

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

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

Equations

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

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

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

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

@[simp]

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

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

Equations

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

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

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

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

@[simp]

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

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

Equations

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

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

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

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

@[simp]

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