val synth_u256 (x: Zeta.Formats.Aux.U256.u256) : Tot Zeta.Steel.LogEntry.Types.u256
val synth_u256 (x: Zeta.Formats.Aux.U256.u256) : Tot Zeta.Steel.LogEntry.Types.u256
let synth_u256
  (x: Zeta.Formats.Aux.U256.u256)
: Tot Zeta.Steel.LogEntry.Types.u256
= Zeta.Steel.LogEntry.Types.Mku256
    x.Zeta.Formats.Aux.U256.v3
    x.Zeta.Formats.Aux.U256.v2
    x.Zeta.Formats.Aux.U256.v1
    x.Zeta.Formats.Aux.U256.v0
module Zeta.Formats.Synth.U256
/
Zeta.Steel.LogEntry.Types.fst.checked Zeta.Formats.Aux.U256.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Formats.Synth.U256.fst
x: Zeta.Formats.Aux.U256.u256 -> Zeta.Steel.KeyUtils.u256
Zeta.Formats.Aux.U256.u256 Zeta.Steel.KeyUtils.Mku256 Zeta.Formats.Aux.U256.__proj__Mku256__item__v3 Zeta.Formats.Aux.U256.__proj__Mku256__item__v2 Zeta.Formats.Aux.U256.__proj__Mku256__item__v1 Zeta.Formats.Aux.U256.__proj__Mku256__item__v0 Zeta.Steel.KeyUtils.u256
let synth_u256 (x: Zeta.Formats.Aux.U256.u256) : Tot Zeta.Steel.LogEntry.Types.u256 =
  
Zeta.Steel.LogEntry.Types.Mku256 x.Zeta.Formats.Aux.U256.v3
  x.Zeta.Formats.Aux.U256.v2
  x.Zeta.Formats.Aux.U256.v1
  x.Zeta.Formats.Aux.U256.v0