diff options
| -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 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) ] + -> [ [<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 ] +. |