Skip to content

Instantly share code, notes, and snippets.

View SlimTim10's full-sized avatar

Tim Johns SlimTim10

View GitHub Profile
@andrejbauer
andrejbauer / AgdaSolver.agda
Last active April 22, 2024 18:20
How to use Agda ring solvers to prove equations?
{- 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