From b338af912c32ab87d6668923add72a56408bddf8 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 May 2015 17:41:45 +0200 Subject: List.nth_error directly produces Some/None instead of value/error List.nth_error and List.hd_error were the only remaining places in the whole stdlib to use type "Exc" instead of "option" directly. So let's simplify things and use option everywhere. In particular, during teaching sessions about lists, we won't have anymore to explain the (lack of) difference between Exc,value,error and option,Some,None. This might cause a few incompatibilities in proof scripts, if they syntactically expect "value" or "error" to occur, but this should hopefully be very rare and quite easy to fix. --- theories/Lists/List.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'theories/Lists') diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 5819fbe5e..e0e5d94d8 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -45,8 +45,8 @@ Section Lists. Definition hd_error (l:list A) := match l with - | [] => error - | x :: _ => value x + | [] => None + | x :: _ => Some x end. Definition tl (l:list A) := @@ -393,11 +393,11 @@ Section Elts. simpl; auto. Qed. - Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A := + Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A := match n, l with - | O, x :: _ => value x + | O, x :: _ => Some x | S n, _ :: l => nth_error l n - | _, _ => error + | _, _ => None end. Definition nth_default (default:A) (l:list A) (n:nat) : A := -- cgit v1.2.3