djspiewak / skolems

A microlibrary for Scala encodings of higher-rank quantifiers
Apache License 2.0
60 stars 8 forks source link

Exists stability and improved unapply #5

Closed wemrysi closed 4 years ago

wemrysi commented 4 years ago

Making the existential value a val instead of a def makes it stable which seems useful, though I don't have concrete example for where it'd be necessary.

Changing the unapply return type allows pattern matching to work in the case where F[_] is a GADT.