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

Equations

• Comparse.NonExtensibleMessageFormat.unit = { parse := fun (b : Bytes) => some ((), b), serialize := fun (x : Unit) => [], parse_wf := ⋯ }

instance Comparse.NonExtensibleMessageFormat.unit.instIsNonAmbiguousUnit {Bytes : Type} [BytesLike Bytes] : unit.IsNonAmbiguous

instance Comparse.NonExtensibleMessageFormat.unit.instHasUniqueRepresentationUnit {Bytes : Type} [BytesLike Bytes] : unit.HasUniqueRepresentation

@[simp]

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

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

Equations

• Comparse.ExtensibleMessageFormat.bytes = { parse := fun (b : Bytes) => some b, serialize := fun (b : Bytes) => b }

instance Comparse.ExtensibleMessageFormat.bytes.instIsNonAmbiguous {Bytes : Type} [BytesLike Bytes] : bytes.IsNonAmbiguous

instance Comparse.ExtensibleMessageFormat.bytes.instHasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] : bytes.HasUniqueRepresentation

@[simp]

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

def Comparse.NonExtensibleMessageFormat.toExtensible {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) : ExtensibleMessageFormat Bytes a

Equations

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

instance Comparse.NonExtensibleMessageFormat.toExtensible.instIsNonAmbiguousOfIsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.IsNonAmbiguous] : mf.toExtensible.IsNonAmbiguous

instance Comparse.NonExtensibleMessageFormat.toExtensible.instHasUniqueRepresentationOfHasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.HasUniqueRepresentation] : mf.toExtensible.HasUniqueRepresentation

@[simp]

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

def Comparse.ExtensibleMessageFormat.toNonExtensible {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (len : Nat) : (∀ (x : a), BytesLike.length (mf.serialize x) = len) → NonExtensibleMessageFormat Bytes a

Equations

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

instance Comparse.ExtensibleMessageFormat.toNonExtensible.instIsNonAmbiguousOfIsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (len : Nat) (h : ∀ (x : a), BytesLike.length (mf.serialize x) = len) [mf.IsNonAmbiguous] : (mf.toNonExtensible len h).IsNonAmbiguous

instance Comparse.ExtensibleMessageFormat.toNonExtensible.instHasUniqueRepresentationOfHasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (len : Nat) (h : ∀ (x : a), BytesLike.length (mf.serialize x) = len) [mf.HasUniqueRepresentation] : (mf.toNonExtensible len h).HasUniqueRepresentation

instance Comparse.ExtensibleMessageFormat.toNonExtensible.instParseConsumesOfNeZeroNat {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (len : Nat) (h : ∀ (x : a), BytesLike.length (mf.serialize x) = len) [NeZero len] : (mf.toNonExtensible len h).ParseConsumes

@[simp]

theorem Comparse.ExtensibleMessageFormat.toNonExtensible.wf_eq {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : ExtensibleMessageFormat Bytes a) (len : Nat) (h : ∀ (x : a), BytesLike.length (mf.serialize x) = len) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : a) : (mf.toNonExtensible len h).wf pred x = mf.wf pred x

def Comparse.NonExtensibleMessageFormat.sigma {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → NonExtensibleMessageFormat Bytes (b x)) : NonExtensibleMessageFormat Bytes (Sigma b)

Equations

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

instance Comparse.NonExtensibleMessageFormat.sigma.instIsNonAmbiguousSigma {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → NonExtensibleMessageFormat Bytes (b x)) [mfa.IsNonAmbiguous] [∀ (x : a), (mfb x).IsNonAmbiguous] : (mfa.sigma mfb).IsNonAmbiguous

instance Comparse.NonExtensibleMessageFormat.sigma.instHasUniqueRepresentationSigma {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → NonExtensibleMessageFormat Bytes (b x)) [mfa.HasUniqueRepresentation] [∀ (x : a), (mfb x).HasUniqueRepresentation] : (mfa.sigma mfb).HasUniqueRepresentation

instance Comparse.NonExtensibleMessageFormat.sigma.instParseConsumesSigma {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → NonExtensibleMessageFormat Bytes (b x)) [mfa.ParseConsumes] : (mfa.sigma mfb).ParseConsumes

instance Comparse.NonExtensibleMessageFormat.sigma.instParseConsumesSigma_1 {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → NonExtensibleMessageFormat Bytes (b x)) [∀ (x : a), (mfb x).ParseConsumes] : (mfa.sigma mfb).ParseConsumes

@[simp]

theorem Comparse.NonExtensibleMessageFormat.sigma.wf_eq {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → NonExtensibleMessageFormat Bytes (b x)) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : Sigma b) : (mfa.sigma mfb).wf pred x = (mfa.wf pred x.fst ∧ (mfb x.fst).wf pred x.snd)

def Comparse.ExtensibleMessageFormat.sigma {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → ExtensibleMessageFormat Bytes (b x)) : ExtensibleMessageFormat Bytes (Sigma b)

Equations

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

instance Comparse.ExtensibleMessageFormat.sigma.instIsNonAmbiguousSigmaOfIsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → ExtensibleMessageFormat Bytes (b x)) [mfa.IsNonAmbiguous] [∀ (x : a), (mfb x).IsNonAmbiguous] : (sigma mfa mfb).IsNonAmbiguous

instance Comparse.ExtensibleMessageFormat.sigma.instHasUniqueRepresentationSigmaOfHasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → ExtensibleMessageFormat Bytes (b x)) [mfa.HasUniqueRepresentation] [∀ (x : a), (mfb x).HasUniqueRepresentation] : (sigma mfa mfb).HasUniqueRepresentation

@[simp]

theorem Comparse.ExtensibleMessageFormat.sigma.wf_eq {Bytes : Type} [BytesLike Bytes] {a : Type} {b : a → Type} (mfa : NonExtensibleMessageFormat Bytes a) (mfb : (x : a) → ExtensibleMessageFormat Bytes (b x)) (pred : Bytes → Prop) [BytesCompatiblePred pred] (x : Sigma b) : (sigma mfa mfb).wf pred x = (mfa.wf pred x.fst ∧ (mfb x.fst).wf pred x.snd)

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

• right_inv (x : b) : f (g x) = some x

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

• left_inv (x : a) : match f x with | none => True | some y => g y = x

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

Equations

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

instance Comparse.NonExtensibleMessageFormat.subsetIsomorphic.instIsNonAmbiguousOfSubsetRightInverse {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → Option b) (g : b → a) [mf.IsNonAmbiguous] [SubsetRightInverse g f] : (mf.subsetIsomorphic f g).IsNonAmbiguous

instance Comparse.NonExtensibleMessageFormat.subsetIsomorphic.instHasUniqueRepresentationOfSubsetLeftInverse {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : NonExtensibleMessageFormat Bytes a) (f : a → Option b) (g : b → a) [mf.HasUniqueRepresentation] [SubsetLeftInverse g f] : (mf.subsetIsomorphic f g).HasUniqueRepresentation

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

@[simp]

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

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

Equations

• mf.subsetIsomorphic f g = { parse := fun (buf : Bytes) => match mf.parse buf with | none => none | some x => f x, serialize := fun (x : b) => mf.serialize (g x) }

instance Comparse.ExtensibleMessageFormat.subsetIsomorphic.instIsNonAmbiguousOfSubsetRightInverse {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → Option b) (g : b → a) [mf.IsNonAmbiguous] [SubsetRightInverse g f] : (mf.subsetIsomorphic f g).IsNonAmbiguous

instance Comparse.ExtensibleMessageFormat.subsetIsomorphic.instHasUniqueRepresentationOfSubsetLeftInverse {Bytes : Type} [BytesLike Bytes] {a b : Type} (mf : ExtensibleMessageFormat Bytes a) (f : a → Option b) (g : b → a) [mf.HasUniqueRepresentation] [SubsetLeftInverse g f] : (mf.subsetIsomorphic f g).HasUniqueRepresentation

@[simp]

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

@[irreducible]

def Comparse.ExtensibleMessageFormat.list.parse {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.ParseConsumes] (buf : Bytes) : Option (List a)

Equations

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

def Comparse.ExtensibleMessageFormat.list.serialize {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) (l : List a) : Bytes

Equations

• Comparse.ExtensibleMessageFormat.list.serialize mf [] = Comparse.BytesLike.empty
• Comparse.ExtensibleMessageFormat.list.serialize mf (h :: t) = Comparse.concatPrefixes (mf.serialize h) (Comparse.ExtensibleMessageFormat.list.serialize mf t)

def Comparse.ExtensibleMessageFormat.list {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.ParseConsumes] : ExtensibleMessageFormat Bytes (List a)

Equations

• Comparse.ExtensibleMessageFormat.list mf = { parse := Comparse.ExtensibleMessageFormat.list.parse mf, serialize := Comparse.ExtensibleMessageFormat.list.serialize mf }

instance Comparse.ExtensibleMessageFormat.list.instIsNonAmbiguousListOfIsNonAmbiguous {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.ParseConsumes] [mf.IsNonAmbiguous] : (list mf).IsNonAmbiguous

instance Comparse.ExtensibleMessageFormat.list.instHasUniqueRepresentationListOfHasUniqueRepresentation {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.ParseConsumes] [mf.HasUniqueRepresentation] : (list mf).HasUniqueRepresentation

@[simp]

theorem Comparse.ExtensibleMessageFormat.list.wf_eq {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.ParseConsumes] (pred : Bytes → Prop) [BytesCompatiblePred pred] (l : List a) : (list mf).wf pred l = ∀ (x : a), x ∈ l → mf.wf pred x

structure Comparse.ListUntil {a : Type} (p : a → Prop) [DecidablePred p] : Type

• init : List { x : a // ¬p x }
• last : { x : a // p x }

@[irreducible]

def Comparse.NonExtensibleMessageFormat.listUntil.parse {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.ParseConsumes] (p : a → Prop) [DecidablePred p] (buf : Bytes) : Option (ListUntil p × Bytes)

Equations

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

def Comparse.NonExtensibleMessageFormat.listUntil.serialize {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.ParseConsumes] (p : a → Prop) [DecidablePred p] (l : ListUntil p) : List Bytes

Equations

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

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

Equations

• mf.listUntil p = { parse := Comparse.NonExtensibleMessageFormat.listUntil.parse mf p, serialize := Comparse.NonExtensibleMessageFormat.listUntil.serialize mf p, parse_wf := ⋯ }

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

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

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

@[simp]

theorem Comparse.NonExtensibleMessageFormat.listUntil.wf_eq {Bytes : Type} [BytesLike Bytes] {a : Type} (mf : NonExtensibleMessageFormat Bytes a) [mf.ParseConsumes] (p : a → Prop) [DecidablePred p] (pred : Bytes → Prop) [BytesCompatiblePred pred] (l : ListUntil p) : (mf.listUntil p).wf pred l = ((∀ (x : { x : a // ¬p x }), x ∈ l.init → mf.wf pred x.val) ∧ mf.wf pred l.last.val)