diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-06 13:27:45 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-06 13:27:45 +0000 |
| commit | f402a7969a656eaf71f88c3413b991af1bbfab0a (patch) | |
| tree | 9062dbbc1d226762fed5a9c324054c65de4002de /theories/Classes/SetoidDec.v | |
| parent | af29dd0dc131674d1cb0007d86b2c12500556aad (diff) | |
Avoid registering λ and Π as keywords just for some private Local Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14459 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidDec.v')
| -rw-r--r-- | theories/Classes/SetoidDec.v | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 762b3fc7d..6708220ea 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -18,9 +18,6 @@ Unset Strict Implicit. Generalizable Variables A B . -Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). - (** Export notations. *) Require Export Coq.Classes.SetoidClass. @@ -93,7 +90,7 @@ Program Instance bool_eqdec : EqDec (eq_setoid bool) := bool_dec. Program Instance unit_eqdec : EqDec (eq_setoid unit) := - λ x y, in_left. + fun x y => in_left. Next Obligation. Proof. @@ -101,8 +98,9 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := reflexivity. Qed. -Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) := - λ x y, +Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) + : EqDec (eq_setoid (prod A B)) := + fun x y => let '(x1, x2) := x in let '(y1, y2) := y in if x1 == y1 then @@ -115,8 +113,9 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq (** Objects of function spaces with countable domains like bool have decidable equality. *) -Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) := - λ f g, +Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) + : EqDec (eq_setoid (bool -> A)) := + fun f g => if f true == g true then if f false == g false then in_left else in_right |