diff options
Diffstat (limited to 'contrib/ring/Setoid_ring.v')
-rw-r--r-- | contrib/ring/Setoid_ring.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v new file mode 100644 index 000000000..59ccc43d3 --- /dev/null +++ b/contrib/ring/Setoid_ring.v @@ -0,0 +1,27 @@ +Require Export Setoid_ring_theory. +Require Export Quote. +Require Export Setoid_ring_normalize. + +Declare ML Module "ring". + +Grammar tactic simple_tactic : ast := + ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))]. + +Syntax tactic level 0: + ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] +| ring_e [ << (Ring) >> ] -> ["Ring"]. + +Grammar vernac vernac : ast := +| addsetoidring [ "Add" "Setoid" "Ring" + constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus) constrarg($amult) + constrarg($aone) constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($pm) + constrarg($mm) constrarg($om) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] + -> [(AddSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aopp $aeq $pm $mm $om $t + ($LIST $l))] +| addsetoidsemiring [ "Add" "Semi" "Setoid" "Ring" + constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus) + constrarg($amult) constrarg($aone) constrarg($azero) constrarg($aeq) + constrarg($pm) constrarg($mm) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] + -> [(AddSemiSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t + ($LIST $l))] +. |