diff options
Diffstat (limited to 'tests/coq/misc/Paper.v')
| -rw-r--r-- | tests/coq/misc/Paper.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 5995de15..661a8cc2 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -9,12 +9,12 @@ Local Open Scope Primitives_scope. Module Paper. (** [paper::ref_incr]: - Source: 'src/paper.rs', lines 4:0-4:28 *) + Source: 'tests/src/paper.rs', lines 4:0-4:28 *) Definition ref_incr (x : i32) : result i32 := i32_add x 1%i32. (** [paper::test_incr]: - Source: 'src/paper.rs', lines 8:0-8:18 *) + Source: 'tests/src/paper.rs', lines 8:0-8:18 *) Definition test_incr : result unit := x <- ref_incr 0%i32; if negb (x s= 1%i32) then Fail_ Failure else Ok tt . @@ -23,7 +23,7 @@ Definition test_incr : result unit := Check (test_incr )%return. (** [paper::choose]: - Source: 'src/paper.rs', lines 15:0-15:70 *) + Source: 'tests/src/paper.rs', lines 15:0-15:70 *) Definition choose (T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) := if b @@ -32,7 +32,7 @@ Definition choose . (** [paper::test_choose]: - Source: 'src/paper.rs', lines 23:0-23:20 *) + Source: 'tests/src/paper.rs', lines 23:0-23:20 *) Definition test_choose : result unit := p <- choose i32 true 0%i32 0%i32; let (z, choose_back) := p in @@ -51,7 +51,7 @@ Definition test_choose : result unit := Check (test_choose )%return. (** [paper::List] - Source: 'src/paper.rs', lines 35:0-35:16 *) + Source: 'tests/src/paper.rs', lines 35:0-35:16 *) Inductive List_t (T : Type) := | List_Cons : T -> List_t T -> List_t T | List_Nil : List_t T @@ -61,7 +61,7 @@ Arguments List_Cons { _ }. Arguments List_Nil { _ }. (** [paper::list_nth_mut]: - Source: 'src/paper.rs', lines 42:0-42:67 *) + Source: 'tests/src/paper.rs', lines 42:0-42:67 *) Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result (T * (T -> result (List_t T))) @@ -82,7 +82,7 @@ Fixpoint list_nth_mut . (** [paper::sum]: - Source: 'src/paper.rs', lines 57:0-57:32 *) + Source: 'tests/src/paper.rs', lines 57:0-57:32 *) Fixpoint sum (l : List_t i32) : result i32 := match l with | List_Cons x tl => i <- sum tl; i32_add x i @@ -91,7 +91,7 @@ Fixpoint sum (l : List_t i32) : result i32 := . (** [paper::test_nth]: - Source: 'src/paper.rs', lines 68:0-68:17 *) + Source: 'tests/src/paper.rs', lines 68:0-68:17 *) Definition test_nth : result unit := let l := List_Cons 3%i32 List_Nil in let l1 := List_Cons 2%i32 l in @@ -107,7 +107,7 @@ Definition test_nth : result unit := Check (test_nth )%return. (** [paper::call_choose]: - Source: 'src/paper.rs', lines 76:0-76:44 *) + Source: 'tests/src/paper.rs', lines 76:0-76:44 *) Definition call_choose (p : (u32 * u32)) : result u32 := let (px, py) := p in p1 <- choose u32 true px py; |