coq.drv 857 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41

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

theory BuiltIn
  syntax type   int     "Z"
  syntax type   real    "R"
  syntax logic  (_=_)   "(%1 = %2)"
  syntax logic  (_<>_)  "(%1 <> %2)"
end


theory int.Int

  prelude "Require ZArith."

  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