diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 15:00:29 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 15:00:29 +0000 |
| commit | 4385c7c73868969617c04f74023ccf944e252bdc (patch) | |
| tree | 7e9af0700633d7d4af95588fcafb54511624762c /theories | |
| parent | 16964be61d6dc240f7539c4a3a66357bb4212cbe (diff) | |
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
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 7 |
1 files changed, 5 insertions, 2 deletions
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]. |