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
IIUC, when writing q($n) for, say n : Nat, it automatically translates $n into ToExpr.toExpr n.
This mechanism doesn't seem to work when we have an antiquotation of generic type \alpha, even if there is an instance of ToExpr \alpha in scope.
import Qq
open Lean
open Qq
-- Worksexample (n : Nat) (m : Q(Nat)) : Q(Nat) :=
q($n)
-- Doesn't workexample {α : Type} [ToExpr α] (a : α) : Expr :=
q($a)
--^^^^^ unknown free variable '_uniq.54'--^^^^^ level mvars not supported ?u.69-- Doesn't work either, but different errorexample {α : Type} [ToExpr α] (a : α) : QQ (toTypeExpr α) :=
q($a)
--^^^^^ unquoteExpr: q.2 : Expr-- Again, doesn't work, but now the error is even on the type declaration, tooexample {α : Type} [ToExpr α] (a : α) : Q($(toTypeExpr α)) :=
-- ^^^^^^^^^^^^^^^^^^ unquoteExpr: ?m.189 : Expr
q($a)
--^^^^^ unquoteExpr: q.2 : Expr
When hovering my cursor over $a (in the Expr-returning example), I see the following context:
«$a»: _uniq.54
⊢ ?m.70
Which seems to suggest that the \alpha type (and the corresponding ToExpr) instance are not part of this local context, explaining why the antiquotation fails.
The text was updated successfully, but these errors were encountered:
IIUC, when writing
q($n)
for, sayn : Nat
, it automatically translates$n
intoToExpr.toExpr n
.This mechanism doesn't seem to work when we have an antiquotation of generic type
\alpha
, even if there is an instance ofToExpr \alpha
in scope.When hovering my cursor over
$a
(in theExpr
-returning example), I see the following context:Which seems to suggest that the
\alpha
type (and the correspondingToExpr
) instance are not part of this local context, explaining why the antiquotation fails.The text was updated successfully, but these errors were encountered: