Note that the above is a simple tautolgogy solver from [2], not tauto
in Coq.
- Agda 2.6.1
- Agda Standard Library v1.0 or above
- My Prelude
Ordered by relevance
-
D. Christiansen and E. Brady, “Elaborator reflection: extending Idris in Idris,” ACM SIGPLAN Not., vol. 51, no. 9, pp. 284–297, Sep. 2016. https://doi.org/10.1145/3022670.2951932
-
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, p. e12, 2015. https://doi.org/10.1017/S0956796815000118
-
J.-O. Kaiser, B. Ziliani, R. Krebbers, Y. Régis-Gianas, and D. Dreyer, “Mtac2: typed tactics for backward reasoning in Coq,” Proc. ACM Program. Lang., vol. 2, no. ICFP, pp. 1–31, 2018. https://doi.org/10.1145/3236773
- Support backward reasoning
- Improve performance
- Add more examples
- Write a paper