diff options
author | Jade Philipoom <jadep@mit.edu> | 2016-01-20 15:54:08 -0500 |
---|---|---|
committer | Jade Philipoom <jadep@mit.edu> | 2016-01-20 15:54:08 -0500 |
commit | 8b3728b68ea21e0cfedfc4eff7fa15830e84bdf1 (patch) | |
tree | 500975efd44b8b78985f8489b6cc5180fceaab0f /coqprime/examples/Make | |
parent | 40750bf32318eb8d93e9537083e4288e55b2555e (diff) |
Import coqprime; use it to prove Euler's criterion.
Diffstat (limited to 'coqprime/examples/Make')
-rw-r--r-- | coqprime/examples/Make | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/coqprime/examples/Make b/coqprime/examples/Make new file mode 100644 index 000000000..7ad748517 --- /dev/null +++ b/coqprime/examples/Make @@ -0,0 +1,18 @@ +-I ../Tactic +-I ../N +-I ../Z +-I ../PrimalityTest +-I ../List +-I ../elliptic +-I ../num + + +BasePrimes.v +PocklingtonRefl.v +TestLucas.v +prime216656403549020227250327256032933021325435259861468456540459488823774358486649614451547405419273433458932168893949521787.v +prime329719147332060395689499.v +russell1.v +russell2.v + + |