Whats the difference between _root_.Nat and Nat?

Stream: new members

[Felipe GS]

-- type mismatch
--   x
-- has type
--   Nat : Type
-- but is expected to have type
--   _root_.Nat : Type

abbrev Dyn := ((α: Type) × α)

def matcher : Dyn → Nat
  | ⟨Nat, x⟩ => x
  | _        => 0

[Yakov Pechersky]

Your second nat is a variable name, not the constant Nat. In vscode, syntax highlighting would color them different. You can't match on Types like this AFAIK. Type equality is undecidable in general.