313abdb49f
This PR fixes the handling of anonymous dependent `if` (`if _ : cond then ... else ...`) inside `do` blocks when using the new do elaborator. The `_%$tk` binder pattern was incorrectly quoted as `$(⟨tk⟩):hole` in the generated `dite` syntax, causing "elaboration function for `termDepIfThenElse` has not been implemented" errors. The fix quotes it correctly as `_%$tk`. A test case is added to verify both anonymous (`if _ : ...`) and named (`if h : ...`) dependent `if` work in do blocks. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
14 lines
402 B
Text
14 lines
402 B
Text
-- Test that anonymous `if _ : cond then ...` works in do blocks (new do elaborator)
|
|
set_option backward.do.legacy false
|
|
def testDepIfAnon (n : Nat) : IO Unit := do
|
|
if _ : n > 0 then
|
|
IO.println "positive"
|
|
else
|
|
IO.println "zero"
|
|
|
|
-- Test the named variant too
|
|
def testDepIfNamed (n : Nat) : IO Unit := do
|
|
if h : n > 0 then
|
|
IO.println s!"positive: {n} > 0"
|
|
else
|
|
IO.println "zero"
|