issues
search
RyanGlScott
/
eliminators
Dependently typed elimination functions using singletons
BSD 3-Clause "New" or "Revised" License
27
stars
0
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Add eliminator for `Symbol`
#8
RyanGlScott
closed
2 years ago
0
Require GHC 8.6
#7
RyanGlScott
closed
6 years ago
0
Emulate Coq's induction schemes for data types that inhabit Prop
#6
RyanGlScott
opened
6 years ago
0
eliminate term-level code
#5
LeanderK
closed
6 years ago
2
Eliminators and Typeclasses
#4
LeanderK
closed
6 years ago
17
Unable to proof per Induction over Nat with Lists
#3
LeanderK
closed
7 years ago
14
Should we bother generating eliminators with predicates of kind (<Datatype> -> Type)?
#2
RyanGlScott
closed
7 years ago
1
Generate eliminators using Template Haskell
#1
RyanGlScott
opened
7 years ago
0