Lucas Escot comments

Repositories
Issues
Comments

Results 34 comments of


                                            Lucas Escot

Name resolution error with `verify`

(Using the latest release `0.29.0`)

Name resolution error with `verify`

Ah thanks. The problem is I also have a separate, parallel model for Cardano, which uses most of the same names. That was my motivation for not importing with `.*`...

Name resolution error with `verify`

Thanks you for the pointers! I guess I will move all my properties to the file the model is defined in, then. Unfortunately, the name resolution does not go away,...

Positivity checker incorrectly marks recursive function as non-recursive.

More or less same example, making implicit arguments explicit: ```agda record S : Set where data Wrap : S → Set where wrap : ∀ {s} → Wrap s id...