diff options
author | Son Ho | 2022-11-14 09:55:13 +0100 |
---|---|---|
committer | Son HO | 2022-11-14 14:21:04 +0100 |
commit | 019a9e34e6375a5e015e4978aad89aa8febc237c (patch) | |
tree | d49947453752ef5ecf17687e02c33c031d91995f /tests/coq/misc/Paper.v | |
parent | 6eab7f1d8eeb7826d44c6bbacf24935965c8f7da (diff) |
Improve the formatting of [if then else] expressions
Diffstat (limited to '')
-rw-r--r-- | tests/coq/misc/Paper.v | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index e15e0dc1..25c01d7b 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -34,13 +34,12 @@ Definition test_choose_fwd : result unit := z0 <- i32_add z 1 %i32; if negb (z0 s= 1 %i32) then Fail_ - else - ( - p <- choose_back i32 true (0 %i32) (0 %i32) z0; - let (x, y) := p in - if negb (x s= 1 %i32) - then Fail_ - else if negb (y s= 0 %i32) then Fail_ else Return tt ) + else ( + p <- choose_back i32 true (0 %i32) (0 %i32) z0; + let (x, y) := p in + if negb (x s= 1 %i32) + then Fail_ + else if negb (y s= 0 %i32) then Fail_ else Return tt) . (** Unit test for [paper::test_choose] *) @@ -61,7 +60,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T := | ListCons x tl => if i s= 0 %u32 then Return x - else ( i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t ) + else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t) | ListNil => Fail_ end . @@ -73,11 +72,10 @@ Fixpoint list_nth_mut_back | ListCons x tl => if i s= 0 %u32 then Return (ListCons ret tl) - else - ( - i0 <- u32_sub i 1 %u32; - tl0 <- list_nth_mut_back T tl i0 ret; - Return (ListCons x tl0) ) + else ( + i0 <- u32_sub i 1 %u32; + tl0 <- list_nth_mut_back T tl i0 ret; + Return (ListCons x tl0)) | ListNil => Fail_ end . |