Time out with the mathematical brackets

Stream: new members

[AHan]

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]

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

[Mario Carneiro]

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]

sorry for a mistake, I think my friend wrote

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

[AHan]

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

[Andrew Ashworth]

Your x in int to pf is an int?

[AHan]

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

[Andrew Ashworth]

You defined p in pf as a nat

[AHan]

But the second example can work?

[Mario Carneiro]

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]

Oh!! Got it! thanks a lot!!