Refactor searching for ornaments (DEVOID)

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

MIT License

49 stars 9 forks source link

Refactor searching for ornaments (DEVOID) #63

Closed tlringer closed 5 years ago

tlringer commented 5 years ago

If name collision issue is too hard to fix on Sunday, consider giving up

tlringer commented 5 years ago

Actually, yeah, just give up Sunday instead

tlringer commented 5 years ago

Will not do. Does not make much sense as a separate plugin. Will just work very nicely with folks who want to use only search code and not lifting code, e.g. in EFF