Zulip Chat Archive

Stream: new members

Topic: Time out with the mathematical brackets


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 ...

view this post on Zulip 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?

view this post on Zulip Andrew Ashworth (Nov 04 2018 at 06:04):

Your x in int to pf is an int?

view this post on Zulip AHan (Nov 04 2018 at 06:24):

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

view this post on Zulip Andrew Ashworth (Nov 04 2018 at 06:30):

You defined p in pf as a nat

view this post on Zulip AHan (Nov 04 2018 at 06:39):

But the second example can work?

view this post on Zulip 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.

view this post on Zulip AHan (Nov 04 2018 at 06:59):

Oh!! Got it! thanks a lot!!


Last updated: May 12 2021 at 05:19 UTC