val xer_ca (xer:xer_t) : bool
let xer_ca = Lemmas.xer_ca
val xer_ca (xer:xer_t) : bool
let xer_ca =
Lemmas.xer_ca
Vale.PPC64LE.Decls.fst.checked
Vale.PPC64LE.StateLemmas.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Print_s.fst.checked Vale.PPC64LE.Memory_Sems.fsti.checked Vale.PPC64LE.Memory.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.Lemmas.fsti.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.IO.fst.checked
Vale.PPC64LE.Decls.fst
Vale.PPC64LE.Lemmas.xer_ca
module Vale.PPC64LE.Decls
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.StateLemmas
module S = Vale.PPC64LE.Semantics_s
module P = Vale.PPC64LE.Print_s
friend Vale.PPC64LE.Memory

let same_heap_types = ()
val xer_ca (xer:xer_t) : bool
xer: Vale.PPC64LE.Machine_s.xer_t -> Prims.bool