search

RyanGlScott / eliminators

Dependently typed elimination functions using singletons
BSD 3-Clause "New" or "Revised" License
27 stars 0 forks source link

Add eliminator for `Symbol` #8

Closed RyanGlScott closed 2 years ago

RyanGlScott commented 2 years ago

eliminators already defines elimNat, which pretends Nat is an inductive data type through clever use of unsafeCoerce. Now that GHC 9.2+ defines a ConsSymbol type family, we can define an analogous eliminator function for Symbol.