diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/misc/Constants.fst | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst index daeefbb0..7bf42b46 100644 --- a/tests/fstar/misc/Constants.fst +++ b/tests/fstar/misc/Constants.fst @@ -20,7 +20,7 @@ let x1_c : u32 = eval_global x1_body let x2_body : result u32 = Return 3 let x2_c : u32 = eval_global x2_body -(** [constants::incr]: forward function +(** [constants::incr]: Source: 'src/constants.rs', lines 17:0-17:32 *) let incr (n : u32) : result u32 = u32_add n 1 @@ -30,7 +30,7 @@ let incr (n : u32) : result u32 = let x3_body : result u32 = incr 32 let x3_c : u32 = eval_global x3_body -(** [constants::mk_pair0]: forward function +(** [constants::mk_pair0]: Source: 'src/constants.rs', lines 23:0-23:51 *) let mk_pair0 (x : u32) (y : u32) : result (u32 & u32) = Return (x, y) @@ -39,7 +39,7 @@ let mk_pair0 (x : u32) (y : u32) : result (u32 & u32) = Source: 'src/constants.rs', lines 36:0-36:23 *) type pair_t (t1 t2 : Type0) = { x : t1; y : t2; } -(** [constants::mk_pair1]: forward function +(** [constants::mk_pair1]: Source: 'src/constants.rs', lines 27:0-27:55 *) let mk_pair1 (x : u32) (y : u32) : result (pair_t u32 u32) = Return { x = x; y = y } @@ -68,7 +68,7 @@ let p3_c : pair_t u32 u32 = eval_global p3_body Source: 'src/constants.rs', lines 49:0-49:18 *) type wrap_t (t : Type0) = { value : t; } -(** [constants::{constants::Wrap<T>}::new]: forward function +(** [constants::{constants::Wrap<T>}::new]: Source: 'src/constants.rs', lines 54:4-54:41 *) let wrap_new (t : Type0) (value : t) : result (wrap_t t) = Return { value = value } @@ -78,7 +78,7 @@ let wrap_new (t : Type0) (value : t) : result (wrap_t t) = let y_body : result (wrap_t i32) = wrap_new i32 2 let y_c : wrap_t i32 = eval_global y_body -(** [constants::unwrap_y]: forward function +(** [constants::unwrap_y]: Source: 'src/constants.rs', lines 43:0-43:30 *) let unwrap_y : result i32 = Return y_c.value @@ -93,12 +93,12 @@ let yval_c : i32 = eval_global yval_body let get_z1_z1_body : result i32 = Return 3 let get_z1_z1_c : i32 = eval_global get_z1_z1_body -(** [constants::get_z1]: forward function +(** [constants::get_z1]: Source: 'src/constants.rs', lines 61:0-61:28 *) let get_z1 : result i32 = Return get_z1_z1_c -(** [constants::add]: forward function +(** [constants::add]: Source: 'src/constants.rs', lines 66:0-66:39 *) let add (a : i32) (b : i32) : result i32 = i32_add a b @@ -118,10 +118,10 @@ let q2_c : i32 = eval_global q2_body let q3_body : result i32 = add q2_c 3 let q3_c : i32 = eval_global q3_body -(** [constants::get_z2]: forward function +(** [constants::get_z2]: Source: 'src/constants.rs', lines 70:0-70:28 *) let get_z2 : result i32 = - let* i = get_z1 in let* i0 = add i q3_c in add q1_c i0 + let* i = get_z1 in let* i1 = add i q3_c in add q1_c i1 (** [constants::S1] Source: 'src/constants.rs', lines 80:0-80:18 *) |