Need help with subtype

Stream: new members

[Kevin Cheung]

I am having trouble doing something very basic with subtype and I hope I could get some help.

In the following, I want quad to be a function that takes a natural number and quadruples it. I want the type signature to be Nat → EvenNat. How does one fix 4 * x to something that Lean will accept?

def EvenNat := { n // ∃ k : Nat, n = 2 * k}

def quad : ℕ → EvenNat := fun x ↦ 4 * x -- Lean naturally complains that this doesn't work.

[Paul Rowe]

An element of a subtype has two parts: the value (which you already provided in your function) and the proof that the value satisfies the required condition (in this case ∃ k : Nat, n = 2 * k). You can write the following:

def quad : ℕ → EvenNat := fun x ↦ ⟨4 * x, ⟨2*x, by ring⟩⟩

[Kevin Cheung]

Ah I see. Thank you!