search

spl / alpha-conversion-is-easy

Lean proof of alpha-conversion is easy
4 stars 0 forks source link

Make “core” definitions private? #11

Closed spl closed 6 years ago

spl commented 6 years ago

Ideally, only the core wrappers would be used, and they would simplify directly into the core implementation.

spl commented 6 years ago

Alternatively, use tactics to generalize and revert such that an extra “core” definition is unnecessary.