<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">Still, library support of general<br>metaprogramming tools is lacking. I also wasn't satisfied by naked and<br>raw De Bruijn indices that Agda uses for its internal representation<br>(which is very error-prone and inefficient) and not having static<br>information on how many times a term was quoted was quite unpleasant,<br>but these are technical details that are pretty solvable. Additional<br>features like defining data types using reflection also can be added.</blockquote><div><br></div><div>A high-level typed tactic language can be implemented via Agda's reflection framework, and I have an</div><div>early implementation of Mtac [1] in Agda as a proof of concept. See <a href="https://github.com/L-TChen/MtacAR" target="_blank">https://github.com/L-TChen/MtacAR</a>.</div><div><br></div><div>Just like Mtac, it gives you pattern matching against expressions, name generation/restriction, abstraction, typed meta variable and reusing Agda's interactive environment. No de Bruijn index manipulation is needed. </div><div><br></div><div>However, it is not ready for "production use" yet. For example, backward reasoning, e.g., Mtac2, requires a cumulative hierarchy of universes to be useful, because subgoals might not be in the same universe. And, the efficiency is pretty bad compared to Agsy, i.e. `C-c C-a`. I am distracted by something else for now, but hopefully it will be actively developed again...</div><div><br></div><div>[1] B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, and V. Vafeiadis, “Mtac: A monad for typed tactic programming in Coq,” J. Funct. Program., vol. 25, Aug. 2015.  DOI: <a href="https://doi.org/10.1017/S0956796815000118" target="_blank">https://doi.org/10.1017/S0956796815000118</a></div></div></div><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div>Best regards,<br></div>Liang-Ting</div></div></div></div></div></div></div>