val stack_to_s (s:vale_stack) : machine_stack
let stack_to_s s = s
val stack_to_s (s:vale_stack) : machine_stack
let stack_to_s s =
s
Vale.PPC64LE.Stack_Sems.fst.checked
Vale.PPC64LE.Stack_i.fst.checked Vale.Lib.Set.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.Classical.fsti.checked
Vale.PPC64LE.Stack_Sems.fst
Vale.PPC64LE.Stack_i.vale_stack Vale.PPC64LE.Machine_s.machine_stack
module Vale.PPC64LE.Stack_Sems
open FStar.Mul

friend Vale.PPC64LE.Stack_i
val stack_to_s (s:vale_stack) : machine_stack
s: Vale.PPC64LE.Stack_i.vale_stack -> Vale.PPC64LE.Machine_s.machine_stack