From eb3fcfee0ff6ddc038998023ac52006073f4724e Mon Sep 17 00:00:00 2001 From: filliatr Date: Mon, 8 Apr 2002 13:40:27 +0000 Subject: syntaxe pour Zdiv et Zmod git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2620 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zdiv.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index d1837e89b4..2d4b9f3720 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) ] + -> [ [ "`"(ZEXPR $n1):E "/" [0 0] (ZEXPR $n2):L "`"] ] + | Zmod [ (Zmod $n1 $n2) ] + -> [ [ "`"(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 ] +. -- cgit v1.2.3