val synth_vbool_recip (x: Zeta.Steel.LogEntry.Types.vbool) : Tot Zeta.Formats.Aux.Vbool.vbool
val synth_vbool_recip (x: Zeta.Steel.LogEntry.Types.vbool) : Tot Zeta.Formats.Aux.Vbool.vbool
let synth_vbool_recip
  (x: Zeta.Steel.LogEntry.Types.vbool)
: Tot Zeta.Formats.Aux.Vbool.vbool
= match x with
  | Zeta.Steel.LogEntry.Types.Vfalse -> Zeta.Formats.Aux.Vbool.Vfalse
  | Zeta.Steel.LogEntry.Types.Vtrue -> Zeta.Formats.Aux.Vbool.Vtrue
module Zeta.Formats.Synth

friend Zeta.Formats.Aux.External.App
friend Zeta.Formats.Aux.External

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

let synth_hash_value_recip
  (x: Zeta.Steel.LogEntry.Types.hash_value)
: Tot Zeta.Formats.Aux.Hash_value.hash_value
= synth_u256_recip x

let synth_vbool
  (x: Zeta.Formats.Aux.Vbool.vbool)
: Tot Zeta.Steel.LogEntry.Types.vbool
= match x with
  | Zeta.Formats.Aux.Vbool.Vfalse -> Zeta.Steel.LogEntry.Types.Vfalse
  | Zeta.Formats.Aux.Vbool.Vtrue -> Zeta.Steel.LogEntry.Types.Vtrue
/
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.Steel.LogEntry.Types.vbool -> Zeta.Formats.Aux.Vbool.vbool
Zeta.Steel.LogEntry.Types.vbool Zeta.Formats.Aux.Vbool.Vfalse Zeta.Formats.Aux.Vbool.Vtrue Zeta.Formats.Aux.Vbool.vbool
let synth_vbool_recip (x: Zeta.Steel.LogEntry.Types.vbool) : Tot Zeta.Formats.Aux.Vbool.vbool =
  
match x with
| Zeta.Steel.LogEntry.Types.Vfalse -> Zeta.Formats.Aux.Vbool.Vfalse
| Zeta.Steel.LogEntry.Types.Vtrue -> Zeta.Formats.Aux.Vbool.Vtrue