## Stream: new members

### Topic: Time out with the mathematical brackets

#### AHan (Nov 04 2018 at 04:11):

I've defined a prime field, and tried to define a function that maps int topf, but somehow timeout at the function...

def pf {p : ℕ} := {e // prime p ∧ 0 ≤ e ∧ e < p}

variable {p : ℕ}

def int_to_pf (x : ℤ) : @pf p := ⟨x, begin end⟩

while my friend succeed with

def pf (p  : ℕ ) [prime p] := {e // 0 ≤ e ∧ e < p}

variable p : ℕ
variable [pp: prime p]

def int_to_pf (x : ℤ) : @pf p (prime p) :=  ⟨x, begin end⟩

Why is there a difference?

#### Mario Carneiro (Nov 04 2018 at 04:34):

you are casting an int to a nat in both examples, this times out searching for a coercion

#### Mario Carneiro (Nov 04 2018 at 04:36):

In the second example it fails fast only because it gets stuck in the type of the theorem: @pf p (prime p) is not well typed because prime p does not have type prime p

#### AHan (Nov 04 2018 at 04:41):

sorry for a mistake, I think my friend wrote

pp: prime p
def int_to_pf (x : ℤ) : @pf p pp ...

#### AHan (Nov 04 2018 at 04:42):

Where did I cast int to nat?
Aren't elements in pf all have value of type nat?

#### Andrew Ashworth (Nov 04 2018 at 06:04):

Your x in int to pf is an int?

#### AHan (Nov 04 2018 at 06:24):

yes, but aren't val of elements of type pf also int?

#### Andrew Ashworth (Nov 04 2018 at 06:30):

You defined p in pf as a nat

#### AHan (Nov 04 2018 at 06:39):

But the second example can work?

#### Mario Carneiro (Nov 04 2018 at 06:51):

lean does not have a subtyping relation, so if something has type pf p it does not have type int. But more importantly you are going the other way around here: x has type int and you are putting it in the first component of pf p, which you didn't write explicitly (it is the type of e) but is nat.

#### AHan (Nov 04 2018 at 06:59):

Oh!! Got it! thanks a lot!!

Last updated: May 12 2021 at 05:19 UTC