Accessing Nat type within inductive Typ

Stream: general

[Cameron Crossman]

I have the following inductive definition
inductive Typ
| Nat
| Fun : Typ → Typ → Typ

and I am trying to write a theorem and start by assuming some variable p is of type Typ.Nat, how do I go about doing so? I get

type expected at
Typ.Nat
term has type
Typ

error from assume p : Typ.Nat or something similar. Thanks!

[Chris Hughes]

Something like this might be what you want

inductive Typ
| Nat : nat → Typ
| Fun : Typ → Typ → Typ

[Chris Hughes]

Hang on.

[Chris Hughes]

Typ.Nat is not a Type, it's a constructor.

[Cameron Crossman]

Oh okay :+1:

[Cameron Crossman]

So I just construct of that type with variable p : Typ.Nat or something along those lines

[Chris Hughes]

Typ.nat : Typ

[Reid Barton]

Typ has nothing to do with actual types, despite the name

[Chris Hughes]

(deleted)

[Reid Barton]

Maybe you want to define an interpretation Typ -> Type

[Cameron Crossman]

thanks!