coq_8_4.drv 793 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7

prelude "(* This file is generated by Why3's Coq 8.4 driver *)"
prelude "(* Beware! Only edit allowed sections below    *)"

printer "coq"
filename "%f_%t_%g.v"

8 9 10
transformation "inline_trivial"
transformation "eliminate_builtin"

MARCHE Claude's avatar
MARCHE Claude committed
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
import "coq-common.gen"

theory real.Trigonometry

  prelude "Require Import Rtrigo."
  prelude "Require Import AltSeries. (* for def of pi *)"

  syntax function cos "(Rtrigo_def.cos %1)"
  syntax function sin "(Rtrigo_def.sin %1)"

  syntax function pi "PI"

  syntax function tan "(Rtrigo1.tan %1)"

  syntax function atan "(Ratan.atan %1)"

  remove prop Pythagorean_identity
  remove prop Cos_le_one
  remove prop Sin_le_one
  remove prop Cos_0
  remove prop Sin_0
  remove prop Cos_pi
  remove prop Sin_pi
  remove prop Cos_pi2
  remove prop Sin_pi2

end