diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-08 13:40:27 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-08 13:40:27 +0000 |
| commit | eb3fcfee0ff6ddc038998023ac52006073f4724e (patch) | |
| tree | 0e4b162ad43622196162a78356f6bcdb14f5a02f | |
| parent | 74f8c29501ad533bf9bb29c22a885f3bd0f10d04 (diff) | |
syntaxe pour Zdiv et Zmod
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2620 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/ZArith/Zdiv.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index d1837e89b..2d4b9f372 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -210,3 +210,25 @@ Split. Rewrite <- Zmult_Zopp_left;Assumption. Rewrite Zabs_non_eq;[Assumption|Omega]. Save. + + +(** Syntax *) + +Grammar znatural expr2 : constr := + expr_div [ expr2($p) "/" expr2($c) ] -> [ (Zdiv $p $c) ] +| expr_mod [ expr2($p) "%" expr2($c) ] -> [ (Zmod $p $c) ] +. + +Syntax constr + level 6: + Zdiv [ (Zdiv $n1 $n2) ] + -> [ [<hov 0> "`"(ZEXPR $n1):E "/" [0 0] (ZEXPR $n2):L "`"] ] + | Zmod [ (Zmod $n1 $n2) ] + -> [ [<hov 0> "`"(ZEXPR $n1):E "%" [0 0] (ZEXPR $n2):L "`"] ] + | Zdiv_inside + [ << (ZEXPR <<(Zdiv $n1 $n2)>>) >> ] + -> [ (ZEXPR $n1):E "/" [0 0] (ZEXPR $n2):L ] + | Zmod_inside + [ << (ZEXPR <<(Zmod $n1 $n2)>>) >> ] + -> [ (ZEXPR $n1):E "%" [0 0] (ZEXPR $n2):L ] +. |