Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Commit c0f89d5

Browse files
committed
fix: don't require know expected type for __dir__/__args__
1 parent f26dbe1 commit c0f89d5

File tree

1 file changed

+8
-2
lines changed

1 file changed

+8
-2
lines changed

Diff for: Lake/DSL/Config.lean

+8-2
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,10 @@ constant dummyArgs : List String
2525
A macro that expands to the path of package's directory
2626
during the Lakefile's elaboration.
2727
-/
28-
scoped elab stx:"__dir__" : term <= expectedType? => do
28+
scoped syntax (name := dirConst) "__dir__" : term
29+
30+
@[termElab dirConst]
31+
def elabDirConst : TermElab := fun stx expectedType? => do
2932
let exp :=
3033
if let some dir := dirExt.getState (← getEnv) then
3134
let str := Syntax.mkStrLit dir.toString (SourceInfo.fromRef stx)
@@ -39,7 +42,10 @@ scoped elab stx:"__dir__" : term <= expectedType? => do
3942
A macro that expands to the configuration arguments passed
4043
via the Lake command line during the Lakefile's elaboration.
4144
-/
42-
scoped elab stx:"__args__" : term <= expectedType? => do
45+
scoped syntax (name := argsConst) "__args__" :term
46+
47+
@[termElab argsConst]
48+
def elabArgsConst : TermElab := fun stx expectedType? => do
4349
let exp :=
4450
if let some args := argsExt.getState (← getEnv) then
4551
quote args

0 commit comments

Comments
 (0)