From 4385c7c73868969617c04f74023ccf944e252bdc Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 22 May 2008 15:00:29 +0000 Subject: writing a match on a digit via syntax "if ... then ... else" is not a good idea :-( (some bad interaction with Arnaud's framework ??) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10969 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Cyclic/Int31/Int31.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'theories') diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 1abd959f9..06248ff7a 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -111,8 +111,11 @@ Definition firstr : int31 -> digits := Eval compute in [ match x with (I31 D0 ... D0) => true | _ => false end ] *) Definition iszero : int31 -> bool := Eval compute in - let f (d:digits)(b:bool) := if d then b else false in - int31_rect _ (nfold_bis _ _ f true size). + let f d b := match d with D0 => b | D1 => false end + in int31_rect _ (nfold_bis _ _ f true size). + +(* NB: DO NOT transform the above match in a nicer (if then else). + It seems to work, but later "unfold iszero" takes forever. *) (** [base] is [2^31], obtained via iterations of [Zdouble]. -- cgit v1.2.3