diff options
author | Jonathan Protzenko | 2022-01-06 10:12:44 -0800 |
---|---|---|
committer | Jonathan Protzenko | 2022-01-06 10:12:44 -0800 |
commit | c3c1d91a976fdac52830239adb6429f09ea888a8 (patch) | |
tree | 15205f3a6356ad80effdc8b48641fff23a89466c /src/Utils.ml | |
parent | 9872966d3c7a97ce8cd9ef16ab934ffa09c23e13 (diff) | |
parent | a310c6036568d8f62e09804c67064686d106afd4 (diff) |
Merge remote-tracking branch 'refs/remotes/origin/main'
Diffstat (limited to '')
-rw-r--r-- | src/Utils.ml (renamed from src/Utilities.ml) | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/Utilities.ml b/src/Utils.ml index 6452d56f..16ee7252 100644 --- a/src/Utilities.ml +++ b/src/Utils.ml @@ -1,7 +1,7 @@ (* Split a list at a given index [i] (the first list contains all the elements up to element of index [i], not included, the second one contains the remaining elements. Note that the first returned list has length [i]. - *) +*) let rec list_split_at (ls : 'a list) (i : int) = if i < 0 then raise (Invalid_argument "list_split_at take positive integers") else if i = 0 then ([], ls) @@ -14,3 +14,10 @@ let rec list_split_at (ls : 'a list) (i : int) = | x :: ls' -> let ls1, ls2 = list_split_at ls' (i - 1) in (x :: ls1, ls2) + +exception Found +(** Utility exception + + When looking for something while exploring a term, it can be easier to + just throw an exception to signal we found what we were looking for. + *) |