Commit graph

55 commits

Author SHA1 Message Date
ce3342f330 deriving 2022-05-02 22:40:28 +02:00
ba3612d836 %default total 2022-05-02 22:38:37 +02:00
9e76bcc765 check quantites of subject and global
- subj qty must be 0 or 1 (atkey)
- global must not be 0 if used at non-0
2022-04-27 22:57:56 +02:00
468c3a4c6a grtt -> qtt 2022-04-27 21:58:09 +02:00
1eace0039e a few tests 2022-04-27 20:06:39 +02:00
5ea7880e38 typechecker stuff 2022-04-24 00:21:30 +02:00
de6ec78e23 add Tighten Term etc 2022-04-12 13:31:46 +02:00
67d8c59cd1 make tighten into an interface 2022-04-11 23:36:01 +02:00
4722e144a3 add ScopeTerm 2022-04-09 15:31:22 +02:00
e6d942ce1b add Dim.toConst 2022-04-06 20:33:00 +02:00
362c9354cf add Var.tighten* 2022-02-27 02:17:51 +01:00
ddba87262d add Injective instances, etc 2022-02-27 02:17:42 +01:00
8248f8ed82 remove some implicits that can now be inferred 2022-02-27 02:06:52 +01:00
3722c769cf add some properties of Var.Compare 2022-02-27 01:50:01 +01:00
c653fcb664 more formatting stuff 2022-02-27 01:49:42 +01:00
e264a18e21 i found an issue about that 0 bug 2022-02-27 01:48:37 +01:00
7d821b20ef add %inline to some instances 2022-02-27 01:47:55 +01:00
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
762ef780af formatting etc 2022-02-27 01:28:19 +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
7bc58625a1 add (?!) for nondependent contexts 2021-12-23 15:58:58 +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
fce293caa7 fix an outdated comment 2021-11-21 14:59:41 +01:00
81fc802fa8 move SomeTerm stuff 2021-09-26 11:11:30 +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
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
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
5baade8dd5 Many => Any 2021-09-03 17:56:07 +02:00
6da33625f8 remove an (.int). no one likes ints 2021-09-03 17:54:52 +02:00
6c05a348d5 formatting fixes & tweaks 2021-09-03 17:10:50 +02:00
d41ab0897c remove some public exports that probably aren't needed 2021-09-03 17:10:24 +02:00
06e5c09896 remove old file i forgot about 2021-09-03 16:57:22 +02:00
45150c2a3b remove zeroes on types 2021-09-03 16:57:22 +02:00