fact: Fixpoint SetCurrentBytes {n sz : nat} {struct sz} : @AlignedEncodeM _ (word (sz * 8)) n := match sz as n0 return (AlignedEncodeM n) with | 0 => AlignedEncode_Nil n | S sz0 => fun v idx w => match sz0 return word (S sz0 * 8) -> _ with | 0 => fun (w' : word 8) => SetCurrentByte v idx w' | S sz1 => fun _ => AppendAlignedEncodeM (fun (v : t Core.char n) (idx : nat) (w : word (S sz0 * 8)) => SetCurrentByte v idx (split1' 8 (sz0 * 8) w)) (fun (v : t Core.char n) (idx : nat) (w : word (S sz0 * 8)) => SetCurrentBytes v idx (split2' 8 (sz0 * 8) w)) v idx w end w end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad