diff options
Diffstat (limited to 'theories/Arith/Arith.v')
| -rwxr-xr-x | theories/Arith/Arith.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 1912f82d0..05fa01f06 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -14,16 +14,17 @@ Axiom My_special_variable : nat -> nat. Grammar nat number :=. -Grammar command command10 := +Grammar constr constr10 := natural_nat [ nat:number($c) ] -> [$c]. -Grammar command atomic_pattern := +Grammar constr pattern := natural_pat [ nat:number($c) ] -> [$c]. Syntax constr level 0: - myspecialvariable [<<My_special_variable>>] -> ["S"]; + myspecialvariable [ My_special_variable ] -> ["S"]; + level 10: - S [<<(S $p)>>] -> [$p:"nat_printer"] -| O [<<O>>] -> [ "0" ] + S [ (S $p) ] -> [$p:"nat_printer"] +| O [ O ] -> [ "0" ] . |