aya-dev icon indicating copy to clipboard operation
aya-dev copied to clipboard

Published 20 hours ago • verified publisher icon aya-prover

Several leftovers of 403

Open ice1000 opened this issue 3 years ago • 1 comments

Several leftovers:

  • [x] I still wish idiom brackets to be desugared in the desugarer, so (| 1 + 2 |) would work.
  • [ ] It would be nice if LocalVar.IGNORED are generated for unused telescopes, but doing so fails the assertion. I think this might mean that we have substitution bugs (maybe we need to formalize everything like Idris2 did...).
  • [ ] There isn't something like do(myBind, myReturn), and we don't have local openings. I guess we may want local openings.

Originally posted by @ice1000 in https://github.com/aya-prover/aya-dev/issues/403#issuecomment-1134983216

ice1000 avatar May 23 '22 18:05 ice1000

I think it makes sense for now to improve the idiom brackets feature and push the others until we have time

ice1000 avatar Aug 30 '22 02:08 ice1000