JovanGerb

Results 57 comments of JovanGerb

fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions

Now you don't need the srcDeclName field anymore right?

fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions

The test file is not currently a module. So I don't see how it is testing what it says it is testing.

fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions

I copy-pasted the test file into the web editor, and it successfully build. Maybe you meant to add `public section` to the test file?

fix: restrict abv positivity extension to variable functions

It's not possible for `f` to be a bvar. Note that `whnf` will panic if it sees a bvar as the head expression.

fix: restrict abv positivity extension to variable functions

Do we also want it to work for a family of functions? I.e. if `f.getAppFn.isFVar`? Otherwise, looks good to me.

feat(to_dual): don't translate the order on `Set`

bors r+

feat: unfold-boundaries in `to_dual`

!bench