Mercurial > hg > Gears > GearsAgda
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 = {!!}