val synth_hash_value (x: Zeta.Formats.Aux.Hash_value.hash_value)
    : Tot Zeta.Steel.LogEntry.Types.hash_value
val synth_hash_value (x: Zeta.Formats.Aux.Hash_value.hash_value)
    : Tot Zeta.Steel.LogEntry.Types.hash_value
let synth_hash_value
  (x: Zeta.Formats.Aux.Hash_value.hash_value)
: Tot Zeta.Steel.LogEntry.Types.hash_value
= synth_u256 x
module Zeta.Formats.Synth

friend Zeta.Formats.Aux.External.App
friend Zeta.Formats.Aux.External
/
Zeta.Steel.LogEntry.Types.fst.checked Zeta.Formats.Aux.Vbool.fsti.checked Zeta.Formats.Aux.Value.fsti.checked Zeta.Formats.Aux.Record.fsti.checked Zeta.Formats.Aux.Mval_value.fsti.checked Zeta.Formats.Aux.Internal_record.fsti.checked Zeta.Formats.Aux.Hash_value.fsti.checked Zeta.Formats.Aux.External.App.fst.checked Zeta.Formats.Aux.External.fst.checked Zeta.Formats.Aux.Descendent_hash_desc.fsti.checked Zeta.Formats.Aux.Descendent_hash.fsti.checked Zeta.Formats.Aux.Application_record_v_payload.fsti.checked Zeta.Formats.Aux.Application_record.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Formats.Synth.fst
x: Zeta.Formats.Aux.Hash_value.hash_value -> Zeta.Steel.LogEntry.Types.hash_value
Zeta.Formats.Aux.Hash_value.hash_value Zeta.Formats.Synth.U256.synth_u256 Zeta.Steel.LogEntry.Types.hash_value
let synth_hash_value (x: Zeta.Formats.Aux.Hash_value.hash_value)
    : Tot Zeta.Steel.LogEntry.Types.hash_value =
  
synth_u256 x