blob: d2229a71baedaa3ed94a62b1df58e4b05cdabbef (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [rename_attribute]: templates for the decreases clauses *)
module RenameAttribute.Clauses.Template
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 56:0-56:27 *)
unfold let factfn_decreases (n : u64) : nat = admit ()
(** [rename_attribute::sum]: decreases clause
Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 *)
unfold
let no_borrows_sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
admit ()
|
