blob: 3bf948d4c57b26a17753dc30c86b4089b2b9b137 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(** [rename_attribute]: the decreases clauses *)
module RenameAttribute.Clauses
open Primitives
open RenameAttribute.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [rename_attribute::factorial]: decreases clause
Source: 'tests/src/rename_attribute.rs', lines 55:0-55:27 *)
unfold let factfn_decreases (n : u64) : nat = n
(** [rename_attribute::sum]: decreases clause
Source: 'tests/src/rename_attribute.rs', lines 64:0-64:27 *)
unfold let no_borrows_sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
if max >= i then max - i else 0
|
