val va_code_Move : dst:va_operand_reg_opr -> src:va_operand_reg_opr -> Tot va_code
let va_code_Move dst src =
  (Ins (S.Move dst src))
val va_code_Move : dst:va_operand_reg_opr -> src:va_operand_reg_opr -> Tot va_code
let va_code_Move dst src =
(Ins (S.Move dst src))
Vale.PPC64LE.InsBasic.fst.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Stack_i.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.Decls.fst.checked Vale.PPC64LE.Decls.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.PPC64LE.InsBasic.fst
Vale.PPC64LE.Decls.va_operand_reg_opr Vale.PPC64LE.Machine_s.Ins Vale.PPC64LE.Decls.ins Vale.PPC64LE.Decls.ocmp Vale.PPC64LE.Semantics_s.Move Vale.PPC64LE.Decls.va_code
module Vale.PPC64LE.InsBasic
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.Memory
open Vale.PPC64LE.Stack_i
friend Vale.PPC64LE.Decls
module S = Vale.PPC64LE.Semantics_s
//-- Move

[@ "opaque_to_smt"]
val va_code_Move : dst:va_operand_reg_opr -> src:va_operand_reg_opr -> Tot va_code
dst: Vale.PPC64LE.Decls.va_operand_reg_opr -> src: Vale.PPC64LE.Decls.va_operand_reg_opr
  -> Vale.PPC64LE.Decls.va_code