I can't ascribe to a named subtype

Stream: lean4

[C7X]

In this MWE, I gave the subtype {n : ℕ // n % 2 == 0} the name NatEven. I can create a member of this type inline, by writing (⟨4, by decide⟩ : NatEven), but when I print out its type, Lean displays {n : ℕ // n % 2 == 0} instead of NatEven. Is this only graphical, and the term really does have type NatEven?

import Mathlib.Data.Nat.Basic

def NatEven : Type := {n : ℕ // n % 2 == 0}

-- The following term does not have type NatEven

#check (⟨4, by decide⟩ : NatEven)

[Aaron Liu]

no, this is just how it works

[Aaron Liu]

a type ascription does not mark the term as having that type

[Aaron Liu]

so inferring the type could give you something different (but still defeq)

[Jireh Loreaux]

use show NatEven from ... to get it to have type NatEven.

[C7X]

Thanks! One more question, is {n : ℕ // n % 2 == 0} definitionally equal to NatEven?

[Aaron Liu]

yes, it is

[Aaron Liu]

definitions are (usually) defeq to their contents

[Aaron Liu]

exceptions for example when you use well-founded recursion

[Kevin Buzzard]

Usually we would write n % 2 = 0 here I guess