From 02ca33e5342ea04ce645a2485938e3082956120b Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Mon, 25 Feb 2019 07:26:26 +1100
Subject: [PATCH] add docstrings explaining the two decidable_prime instances

---
 src/data/nat/prime.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/data/nat/prime.lean b/src/data/nat/prime.lean
index 2c8066174c219..2f053890a631b 100644
--- a/src/data/nat/prime.lean
+++ b/src/data/nat/prime.lean
@@ -53,6 +53,14 @@ prime_def_lt'.trans $ and_congr_right $ λ p2,
       rwa [one_mul, ← e] }
   end⟩
 
+/--
+  This instance is slower than the instance `decidable_prime` defined below,
+  but has the advantage that it works in the kernel.
+
+  If you need to prove that a particular number is prime, in any case
+  you should not use `by dec_trivial`, but rather `by norm_num`, which is
+  much faster.
+  -/
 def decidable_prime_1 (p : ℕ) : decidable (prime p) :=
 decidable_of_iff' _ prime_def_lt'
 local attribute [instance] decidable_prime_1
@@ -190,6 +198,15 @@ section min_fac
     ((dvd_prime pp).1 fd).resolve_left (ne_of_gt f2)⟩,
    λ ⟨p2, e⟩, e ▸ min_fac_prime (ne_of_gt p2)⟩
 
+  /--
+  This instance is faster in the virtual machine than `decidable_prime_1`.
+  However it uses `classical.choice`, so can't actually be used in a
+  decision procedure.
+
+  If you need to prove that a particular number is prime, in any case
+  you should not use `by dec_trivial`, but rather `by norm_num`, which is
+  much faster.
+  -/
   instance decidable_prime (p : ℕ) : decidable (prime p) :=
   decidable_of_iff' _ prime_def_min_fac