diff options
| author | Son Ho | 2023-03-07 17:49:03 +0100 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | 4db56fe2c963a4052f8415b3985c8765407fccbc (patch) | |
| tree | 53c5f05469bb3946547c418176f35d840dbe6012 /tests/lean/hashmap_on_disk/HashmapMain/Clauses | |
| parent | 051e2a19f3268d272a0acd0425d2107ebea020c5 (diff) | |
Update the extraction of Lean files
Diffstat (limited to 'tests/lean/hashmap_on_disk/HashmapMain/Clauses')
| -rw-r--r-- | tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean index 16a4ea4c..a514c58a 100644 --- a/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean +++ b/tests/lean/hashmap_on_disk/HashmapMain/Clauses/Clauses.lean @@ -1,11 +1,12 @@ --- [hashmap_main]: decreases clauses +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: templates for the decreases clauses import Base.Primitives import HashmapMain.Types /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots]: termination measure -/ @[simp] def hashmap_hash_map_allocate_slots_loop_terminates (T : Type) - (slots : vec (hashmap_list_t T)) (n : USize) := + (slots : Vec (hashmap_list_t T)) (n : USize) := (slots, n) syntax "hashmap_hash_map_allocate_slots_loop_decreases" term+ : tactic @@ -14,16 +15,17 @@ macro_rules | `(tactic| hashmap_hash_map_allocate_slots_loop_decreases $slots $n) => `(tactic| sorry) -/- [hashmap_main::hashmap::HashMap::{0}::clear]: termination measure -/ +/- [hashmap_main::hashmap::HashMap::{0}::clear_slots]: termination measure -/ @[simp] -def hashmap_hash_map_clear_loop_terminates (T : Type) - (slots : vec (hashmap_list_t T)) (i : USize) := +def hashmap_hash_map_clear_slots_loop_terminates (T : Type) + (slots : Vec (hashmap_list_t T)) (i : USize) := (slots, i) -syntax "hashmap_hash_map_clear_loop_decreases" term+ : tactic +syntax "hashmap_hash_map_clear_slots_loop_decreases" term+ : tactic macro_rules -| `(tactic| hashmap_hash_map_clear_loop_decreases $slots $i) =>`(tactic| sorry) +| `(tactic| hashmap_hash_map_clear_slots_loop_decreases $slots $i) => + `(tactic| sorry) /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: termination measure -/ @[simp] @@ -52,7 +54,7 @@ $ls) =>`(tactic| sorry) /- [hashmap_main::hashmap::HashMap::{0}::move_elements]: termination measure -/ @[simp] def hashmap_hash_map_move_elements_loop_terminates (T : Type) - (ntable : hashmap_hash_map_t T) (slots : vec (hashmap_list_t T)) (i : USize) + (ntable : hashmap_hash_map_t T) (slots : Vec (hashmap_list_t T)) (i : USize) := (ntable, slots, i) |