- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
Ltac solveInstr :=
unfold mov, ldr,
str, cmp,
jnz, jmp, halt, fail,
hvc, run, yield, share, lend, donate,
retrieve, relinquish, reclaim, send, wait,
option_state_unpack, unpack_hvc_result_normal, unpack_hvc_result_yield,
get_reg, update_reg, update_incr_PC, get_memory, update_memory;
repeat case_match;
subst; eauto.