af120501a9
Getting UnappendR back using some casts
03c77d8116
Add SnocList and Queue (WIP)
f80172ad9e
Comment out the inference of the right context from the whole context and the left context
51b161b2cc
Fix typo
73bc7fb9d1
Fix a bug in act
d55eaae5ec
Add semantics of CBPV in EM categories
52a0b20e26
Add the CBN to CBPV embedding
7ba967c826
Add syntax for CBPV
c102cad8ac
Add Adj and CoPow
1fb84ff56a
Update README
acb23765c8
Small refactoring
f8e642a04a
Finish refactoring
0f963a2e32
Change README
5fbea1cb3b
Create .cabal file
f946eec5d4
Refactor LType
180fb027bf
Add an interpretation into ordinary types
d5628ea83d
Add a nicer interface for embed
781a650171
Refactor linear connectives so that the primitive API do not have the fancy constraints
33f7251fd3
Add
cases
d4c891a7b6
Add absurd elimination