Noob Question: How to encode 'there are infinitely many primes' in F*

[fwaris]

Got upto to the following but I can't find a why to define 'pime' in F*.

module Welcome
open FStar.Math.Lib

val prime : nat -> Type

let infinitely_many_primes : prop =
  forall (n:nat) . exists(p:nat) . prime p /\ p >= n

Something like the following for prime is not accepted:

let divides (d n:nat) : prop =
  exists (k:nat) . n == d * k

let prime (p:nat) : prop =
  p >= 2 /\
  (forall (d:nat) . divides d p ==> d == 1 \/ d == p)

For the above, at d * k gives the error at d:

- Expected expression of type Type got expression d of type nat
- See also <input>(6,13-6,14)
F*

[mtzguido]

This is a common gotcha: by default * denotes the tuple type constructor, so something like int * int is a pair of ints. We mostly write int & int these days, but the default interpretation is still to take * as the tuple constructor.

To make * denote multiplication, you can open the FStar.Mul module which defines the following alias: unfold let op_Star = Prims.op_Multiply. Or you can use op_Multiply directly too.

[fwaris]

thanks! that was it. I will now go through the tutorials to get the basics in order.