Next possible steps for the MetaAya project...

[lunalunaa]

Priority 0 (enhancements):

• More tests
• Separate everything related to tactic out into another class, something like TacticElaborator
• LSP integration

---

Priority 1 (new features):

• Implement syntactic reflection and quasiquoting
• Idris-style monadic elaborator reflection (requires a monadic infrastructure)
• Coq/lean-style tactic

---

Priority 2 (research):

• Performance benchmarking and optimization
• MTac(2)-style well-typed metaprogramming

---

Priority ∞:

• Formalized metatheory of Aya, in Aya: Aya Aya Accept!

[ice1000]

I propose TacticElaborator -> TacticTycker or TacTycker