coq.drv 937 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5

printer "coq"
filename "%f_%t_%s.v"
call_on_file "coqc %s"

MARCHE Claude's avatar
MARCHE Claude committed
6 7


MARCHE Claude's avatar
MARCHE Claude committed
8
theory BuiltIn
MARCHE Claude's avatar
MARCHE Claude committed
9 10 11 12

  prelude "Require Import ZArith."
  prelude "Require Import Rbase."

MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16 17 18 19 20 21
  syntax type   int     "Z"
  syntax type   real    "R"
  syntax logic  (_=_)   "(%1 = %2)"
  syntax logic  (_<>_)  "(%1 <> %2)"
end


theory int.Int

MARCHE Claude's avatar
MARCHE Claude committed
22
  prelude "Require Import ZArith."
MARCHE Claude's avatar
MARCHE Claude committed
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47

  syntax logic zero "0%Z"
  syntax logic one "1%Z"

  syntax logic (_+_) "(%1 + %2)%Z"
  syntax logic (_-_) "(%1 - %2)%Z"
  syntax logic (_*_) "(%1 * %2)%Z"
  syntax logic (-_)  "(-%1)%Z"

  syntax logic (_<=_) "(%1 <= %2)%Z"
  syntax logic (_<_) "(%1 <  %2)%Z"
  syntax logic (_>=_) "(%1 >= %2)%Z"
  syntax logic (_>_) "(%1 >  %2)%Z"

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary

end