rekenaar
rekenaar copied to clipboard
jdevuyst
Idris tactics for (commutative) monoids
Results
2
rekenaar issues
Sort by
recently updated
recently updated
newest added
This looks interesting: https://github.com/oisdk/agda-ring-solver/
The following code ``` plusCommutativeRewrite' : (l, r : Nat) -> Fin (l + r) -> Fin (r + l) plusCommutativeRewrite' = %runElab (do rewriter {ty=`(Nat)} natPlusRefl) ``` fails with...
