This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- Here is a short demonstration on how to use Agda's solvers that automatically | |
prove equations. It seems quite impossible to find complete worked examples | |
of how Agda solvers are used. | |
Thanks go to @anormalform who helped out with these on Twitter, see | |
https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng | |
I welcome improvements and additions to this file. | |
This file works with Agda 2.6.2.2 and standard-library-1.7.1 |