diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-28 16:28:56 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-31 10:03:57 -0400 |
| commit | b52edcb4a5ba5757b3a384997d501611aa1feb00 (patch) | |
| tree | 22ca8210557af7b2c31b1deb7cbe15a38ff60692 /src/ModularArithmetic | |
| parent | 9ffba573db9c809f53ed422e9cc4e4fab69693b9 (diff) | |
fixed typo; extra argument
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 5e5b82d0f..b8256f5a8 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -89,7 +89,7 @@ Section ModularBaseSystem. Definition sqrt_3mod4 (chain : list (nat * nat)) (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 4 + 1)) - (sqrt_minus1 x : digits) : digits := pow x chain. + (x : digits) : digits := pow x chain. Import Morphisms. Global Instance eq_Equivalence : Equivalence eq. |