search

frex-project / idris-frex

Other
46 stars 9 forks source link

First stab at frex pretty printer #40

Closed ohad closed 3 years ago

ohad commented 3 years ago

(defo need to clean up first, but just checking what those proofs look like for commutative monoids)

gallais commented 3 years ago

I'm not sure I understand why we don't need the Nary.curry anymore. How is the environment magically reconstructed?

ohad commented 3 years ago

We don't need the environment since we're manipulating an element of the free extension.

Since the 'dynamic' elements are going to usually be actual variable names / stuck computations, I don't expect we'll need the environment when printing. But if I'm proven wrong in the future, we can refactor!