|
7faca8ac27
|
use Subset instead of relevant product
|
2022-04-11 23:34:28 +02:00 |
|
|
d912614d7d
|
fiddling
|
2022-04-11 23:34:18 +02:00 |
|
|
25f4923fac
|
merge duplicate Nat LTE'
|
2022-04-11 23:33:32 +02:00 |
|
|
38260d3838
|
producing a proof in TC is not worth it
|
2022-04-08 03:47:53 +02:00 |
|
|
8248f8ed82
|
remove some implicits that can now be inferred
|
2022-02-27 02:06:52 +01:00 |
|
|
9bd02d185a
|
add Context.pure
|
2022-02-27 01:28:36 +01:00 |
|
|
762ef780af
|
formatting etc
|
2022-02-27 01:28:19 +01:00 |
|
|
3efff3e96d
|
rewrite Context.(!!)
|
2022-02-27 01:22:05 +01:00 |
|
|
a11e4d5ef1
|
add LT/LTE for vars
|
2021-12-23 19:01:24 +01:00 |
|
|
1924250fcd
|
add lengthPrf0 for contexts
|
2021-12-23 16:03:49 +01:00 |
|
|
7bc58625a1
|
add (?!) for nondependent contexts
|
2021-12-23 15:58:58 +01:00 |
|
|
2a5b8ec815
|
bikeshedding
|
2021-12-23 15:55:18 +01:00 |
|
|
dbd0a3a451
|
add name to type arg in Context' and Telescope'
|
2021-12-23 15:54:16 +01:00 |
|
|
37230a8032
|
tweak some type signatures
|
2021-11-21 14:59:27 +01:00 |
|
|
36b3479c8d
|
more context stuff
|
2021-09-25 20:11:29 +02:00 |
|
|
e0bf8fa795
|
add context stuff
|
2021-09-09 23:56:10 +02:00 |
|