blob: 8bc3d6e209cb350c7fe7f463841676338c3ddd32 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import ZModulo.
(**
* The relevant module is ZModulo:
* the constructor you want is of_pos
* the operations you want are in zmod_ops
* the tactics you want are somewhere between Field and CyclicType:
* probs you want to be converting to/from Z pretty frequently
*
* Coq Reference page:
* https://coq.inria.fr/library/Coq.Numbers.Cyclic.ZModulo.ZModulo.html
*)
|
