Writing a function that returns (Nat, Type)

Stream: new members

[Tomaz Gomes Mascarenhas]

Hi,
I want to write a function that returns a pair in which each coordinate have a different Sort (for instance, (Nat, Type)), but Lean gives me the error:

type expected
failed to synthesize instance
  CoeSort (Type × Type 1) ?m.451

but if I try #check (Nat, Type) I can actually get an answer:

(Nat, Type) : Type × Type 1

Is there a way to write such a function?

[Riccardo Brasca]

Can you write a #mwe?

[Arthur Paulino]

Can you post the code you've got so far?

[Reid Barton]

(Nat, Type) is a pair not a type--did you mean a function that returns Nat × Type?

[Tomaz Gomes Mascarenhas]

yes, you're right, thank you!