hex

3.3. The primality tactic🔗

The bare tactic closes a Hex.Nat.Prime goal on a numeral; the search runs compiled at elaboration time and the kernel replays only the certificate check:

example : Hex.Nat.Prime 2147483647 := ⊢ Hex.Nat.Prime 2147483647 All goals completed! 🐙

It is also a term elaborator, and with an explicit numeral in tactic mode it adds a hypothesis (this, or a chosen name):

example : Hex.Nat.Prime 2147483647 := primality 2147483647 example : True := ⊢ True this:Hex.Nat.Prime 65537⊢ True this:Hex.Nat.Prime 65537fermat:Hex.Nat.Prime 257⊢ True All goals completed! 🐙

On a composite input the tactic fails with the witness that refutes primality:

example : Hex.Nat.Prime 561 := primality: 561 is not prime (Miller-Rabin witness 2)primality 561 
primality: 561 is not prime (Miller-Rabin witness 2)