# Zulip Chat Archive

## 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`

to`pf`

, 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