Commit graph

513 commits

Author SHA1 Message Date
76c02adf03 add Subst.one 2022-02-27 01:47:25 +01:00
3ea9db1c82 export bodies of CanShift instances and rename Compose to Map 2022-02-27 01:47:25 +01:00
d8f869d6df some DimEqs properties 2022-02-27 01:47:25 +01:00
7ea494c3cd add some whnf stuff 2022-02-27 01:47:25 +01:00
9b260529c8 add casts to Integer for Var & Shift 2022-02-27 01:36:08 +01:00
610b5fde2d add DimEqs.get etc 2022-02-27 01:33:52 +01:00
8006ae4c40 add DimEqs.zeroEq 2022-02-27 01:31:52 +01:00
d52d1c3181 add %inlines 2022-02-27 01:30:23 +01:00
bc3230e000 rename Error.inj to one 2022-02-27 01:28:49 +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
88338050fc start of type stuff 2021-12-23 19:05:50 +01:00
f363dc3122 add DimEq 2021-12-23 19:05:00 +01:00
730cedc4c0 wap quantities in pi to match grtt 2021-12-23 19:03:37 +01:00
b5cfc7b23b add pushSubsts' to just have the term without proof 2021-12-23 19:03:04 +01:00
568dba6f0b CanShift Dim 2021-12-23 19:01:39 +01:00
a11e4d5ef1 add LT/LTE for vars 2021-12-23 19:01:24 +01:00
acfa1b96be bikeshedding again 2021-12-23 16:05:55 +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
c75332be44 remove old typecheck stuff 2021-12-23 15:53:40 +01:00
e833322ebe add separate type for dimension endpoints 2021-12-23 15:52:56 +01:00
40fde92823 change printing of binders
old: (1 | 1 | x : A) ->
new: (x @ 1, 1 : A) ->
2021-12-23 15:50:19 +01:00
d5530f9884 remove Eval.idr which is no good 2021-11-29 14:50:53 +01:00
fce293caa7 fix an outdated comment 2021-11-21 14:59:41 +01:00
37230a8032 tweak some type signatures 2021-11-21 14:59:27 +01:00
81fc802fa8 move SomeTerm stuff 2021-09-26 11:11:30 +02:00
65e45dcc79 use stdlib Elem and add note why not also stdlib OpenUnion 2021-09-26 10:55:07 +02:00
2b1a043280 beginnings of typechecker, maybe 2021-09-25 20:24:23 +02:00
11856fa96a eval stuff 2021-09-25 20:24:04 +02:00
a5b07672ae renaming etc in closure stuff 2021-09-25 20:14:13 +02:00
eae97a7b9d reorder clauses in Subst.(.) 2021-09-25 20:13:51 +02:00
cdcd926347 improve error interfaces 2021-09-25 20:13:13 +02:00
36b3479c8d more context stuff 2021-09-25 20:11:29 +02:00
f87950915d add more bib entries 2021-09-25 20:10:30 +02:00
83ad802f6e add fancy error monad 2021-09-20 09:32:02 +02:00
4da8aa6031 start of eval module but not really 2021-09-09 23:56:29 +02:00
e0bf8fa795 add context stuff 2021-09-09 23:56:10 +02:00
3f11530336 rename isCloX to topCloX 2021-09-09 23:55:49 +02:00
4a2f7e1497 add CanSubst Var (Term/Elim) 2021-09-09 23:55:30 +02:00
8c675d01d5 make (//) lazier 2021-09-09 23:54:40 +02:00
b29c56e0ae fixup! fix import in main 2021-09-09 23:53:37 +02:00
a2be5a468d add CanShift interface like CanSubst 2021-09-09 23:53:00 +02:00
b29b7855a2 make IsQty interface 2021-09-09 23:51:45 +02:00
b47ef502f3 inline 2021-09-09 23:51:29 +02:00
b29fd538e4 fix import in main 2021-09-09 23:51:00 +02:00
5baade8dd5 Many => Any 2021-09-03 17:56:07 +02:00