diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 18:27:52 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 18:27:52 +0000 |
commit | a67717d7989cf6bb296d67550fd09dcfe727f727 (patch) | |
tree | 37285a1f53db7abefe61ed26f4f462abd4ab4032 /contrib/field/Field_Compl.v | |
parent | 6c892e6e04be39385e2338b973bf108a05836153 (diff) |
MAJ syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3233 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/field/Field_Compl.v')
-rw-r--r-- | contrib/field/Field_Compl.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v index 514edf39c..edf079317 100644 --- a/contrib/field/Field_Compl.v +++ b/contrib/field/Field_Compl.v @@ -22,10 +22,11 @@ Inductive Sprod [A:Type;B:Set] : Type := Spair : A -> B -> (Sprod A B). Definition assoc_2nd := -Fix assoc_2nd_rec {assoc_2nd_rec/4: - (A:Type)(B:Set)((e1,e2:B){e1=e2}+{~e1=e2})->(listT (Sprod A B))->B->A->A:= - [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(listT (Sprod A B)); - key:B;default:A] +Fix assoc_2nd_rec + {assoc_2nd_rec + [A:Type;B:Set;eq_dec:(e1,e2:B){e1=e2}+{~e1=e2};lst:(listT (Sprod A B))] + : B->A->A:= + [key:B;default:A] Cases lst of | nilT => default | (consT (Spair v e) l) => @@ -49,8 +50,7 @@ Definition sndT [A,B:Type;c:(prodT A B)] := end. Definition mem := -Fix mem {mem/4:(A:Set)((e1,e2:A){e1=e2}+{~e1=e2})->(a:A)(listT A)->bool := - [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)] +Fix mem {mem [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)] : bool := Cases l of | nilT => false | (consT a1 l1) => |