diff ModelChecking.agda @ 637:e30dcd03c07f

stack invariant in findP
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 Nov 2021 15:04:06 +0900
parents 1c8dca459d9a
children 4761b08c4bd6
line wrap: on
line diff
--- a/ModelChecking.agda	Sun Nov 14 15:50:30 2021 +0900
+++ b/ModelChecking.agda	Mon Nov 15 15:04:06 2021 +0900
@@ -65,7 +65,7 @@
 putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next = C_putdown_lfork } )
 
 code_table :  {n : Level} {t : Set n} → Code → Process → ( Process → t) → t
-code_table C_set  = ?
+code_table C_set  = {!!}
 code_table C_putdown_rfork = putdown_rfork_stub
 code_table C_putdown_lfork = {!!}
 code_table C_thinking = {!!}