blob: 4290d8fff039626a9af9f48f848a05a7f079e30d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
From Sail Require Import State_monad State_lifting.
Require Import String.
Require Import List.
Import ListNotations.
Goal True.
let result := eval cbv in (liftState register_accessors (main tt) (init_state tt)) in
match result with
| [(Value tt,_)] => idtac "OK"
| [(Ex (Failure ?s),_)] => idtac "Fail:" s
| _ => idtac "Fail"
end.
exact I.
Qed.
|
