From d0e33a5cfc4aaff4d5f733319f1631855b592cc6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hu=E1=BB=B3nh=20Tr=E1=BA=A7n=20Khanh?= Date: Tue, 14 Nov 2023 10:46:15 +0700 Subject: [PATCH] Fix indent --- theories/Imperative.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Imperative.v b/theories/Imperative.v index 4f00edd..c28871b 100644 --- a/theories/Imperative.v +++ b/theories/Imperative.v @@ -21,7 +21,7 @@ Proof. - case b as [| effect2 continuation2]. + exact False. + pose proof (ltac:(intro hEffect; subst effect; exact (forall response, identical _ _ _ (continuation response) (continuation2 response))) : effect = effect2 -> Prop) as rhs. - exact (effect = effect2 /\ forall x: effect = effect2, rhs x). + exact (effect = effect2 /\ forall x: effect = effect2, rhs x). Defined. Fixpoint bind {effectType effectResponse A B} (a : Action effectType effectResponse A) (f : A -> Action effectType effectResponse B) : Action effectType effectResponse B :=