Skip to content

Commit c79de11

Browse files
febyejibensimner
authored andcommitted
(rocq-checker) remove the unused code
1 parent 86f3f3a commit c79de11

File tree

2 files changed

+0
-29
lines changed

2 files changed

+0
-29
lines changed

src/casemate-check-rocq/addr_test.sh

Lines changed: 0 additions & 21 deletions
This file was deleted.

src/casemate-check-rocq/theories/utils.v

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -165,14 +165,6 @@ Inductive internal_error_type :=
165165
| IET_no_write_authorization
166166
.
167167

168-
Fixpoint nth_opt {A : Type} (n : nat) (l : list A) {struct l} : option A :=
169-
match n, l with
170-
| O, x :: l' => Some x
171-
| O, _ => None
172-
| S m, nil => None
173-
| S m, x :: t => nth_opt m t
174-
end.
175-
176168
Fixpoint idx_of {A : Type} (f : A -> bool) (acc : nat) (l : list A) {struct l} : nat :=
177169
match l with
178170
| nil => acc

0 commit comments

Comments
 (0)