Certificates extraction for MonoidTheory

frex-project / idris-frex

Other

46 stars 9 forks source link

Closed gallais closed 3 years ago

gallais commented 3 years ago

Starting with the special case of monoids, and in particular ((Nat, Equal), 0, +).

NB: Printer test case for commutative monoids is currently broken following a big refactoring.

ohad commented 3 years ago

I merged from the setoid reasoning PR #47 .

Shall we remove #47 and keep this one only, or will gh be able to deal with both merges?

gallais commented 3 years ago

Let's see! :ship: