You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
lakefile: require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
imported and opened Qq fine; simple examples work but:
similarly, it seems that the List ((u : Level) × (α : Q(Sort u)) × List Q(Option $α)) example doesn't work. The cause for this seems to be that Option takes a Type argument, not a Sort one.
lakefile:
require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
imported and opened Qq fine; simple examples work but:
def betterApp {α : Q(Sort u)} {β : Q($α → Sort v)} (f : Q((a : α) → $β a)) (a : Q($α)) : Q($β $a) := q($f $a)
error in Q((a : α) → $β a)) reported:
unsupported implicit auto-bound: α is not a level name
humble apologies if this is a simple user error!
The text was updated successfully, but these errors were encountered: