macro to construct ( $tm : $ty)

Stream: new members

[Mark Aagaard]

I am trying to construct a macro that takes a term tm and a type ty, then constructs the term `( ($tm:$ty)). I can get the individual steps to work, but not the whole thing:

macro "tycheck2" tm:term : term => `( ($tm : Nat))
#check tycheck2 4 -- OK: pass in just the term

macro "tycheck3" ty:term : term => `( (4 : $ty))
#check tycheck3 Nat -- OK: pass in just the type

macro "tycheck4" tm:term ty:term : term => `( ($tm : $ty) )
#check tycheck4 4 Nat  -- FAIL with error message "unexpected end of input"

What's the best way to construct a type assertion from two terms?

-mark

[Kyle Miller]

The problem here isn't in the construction, but in the syntax definition. There's an ambiguity: 4 Nat is a valid term, so tm matches that.

[Kyle Miller]

Try doing tm:term:arg and ty:term:arg to set the ambient precedences of those terms to be at the argument level

[Kyle Miller]

arg level can't match 4 Nat, just 4.

[Mark Aagaard]

Kyle-
Thanks, that makes sense.
-mark