Stephen Chang
84108c7300
start some eq tests; fix dep-ind (in dep-ind-fixed) so indices can depend on params
2017-09-19 16:03:07 -04:00
Stephen Chang
8eb637af0e
add universes where Type n : Type n+1
2017-08-31 15:31:54 -04:00
Stephen Chang
1042a27b62
code cleanup
2017-08-23 14:09:07 -04:00
Stephen Chang
c6b315742c
restore some lost types after reductions
2017-08-23 12:45:12 -04:00
Stephen Chang
47dc16e68a
Vect and vappend working!
2017-08-22 17:17:05 -04:00
Stephen Chang
98327386ae
indexed vectors basic example working
2017-08-18 16:04:46 -04:00
Stephen Chang
24d694cf46
for tycons, make all args explicit (eg tyvars) for all elim args
2017-08-17 19:13:59 -04:00
Stephen Chang
f7b90e0473
define-datatype supports tycons, eg lists
2017-08-17 18:17:33 -04:00
Stephen Chang
804c82bf24
add dep-ind example with define-datatype
2017-08-16 12:39:28 -04:00
Stephen Chang
7fc8bd8c15
rename dep2 requires -> dep
2017-08-14 13:51:41 -04:00
Stephen Chang
fcc9429932
rename dep2 -> dep
2017-08-14 13:50:50 -04:00
Stephen Chang
441ec0e5d7
remove dep example
2017-08-14 13:48:53 -04:00
Stephen Chang
7c841dc750
omit dep-tests from tests
2017-08-04 15:18:07 -04:00
Stephen Chang
eae7e14c44
add dep2-assist
2017-08-04 14:31:29 -04:00
Stephen Chang
bbb6b0a694
add nat-ind, nat-rec, right/left plus id examples
2017-08-04 12:15:32 -04:00
Stephen Chang
3fd22a9058
add eq-elim and more equality proof examples
2017-08-02 14:58:27 -04:00
Stephen Chang
79e84d6fd5
add eq-refl; app/eval seems to work
2017-08-01 17:08:30 -04:00
Stephen Chang
31bc8cebec
add bool and nat examples; start eq-refl; need to fix app/eval
2017-07-31 19:37:04 -04:00
Stephen Chang
4e80959d12
start over with dep2; basic lam/app working; no instantiation
2017-07-31 16:35:33 -04:00
Stephen Chang
ac832bced0
inst args
2017-07-26 15:39:07 -04:00
Stephen Chang
05f65c13d8
add nat tests; start peano nums; nat-ind not working
2017-07-26 15:39:07 -04:00
Milo Turner
fe5adac3db
add define-typed-variable-syntax
...
closes #13
2017-07-25 13:18:40 -04:00
Stephen Chang
39be2ef904
fix #16
2017-07-24 12:01:40 -04:00
Milo
2d6ecae8c4
added #:mode and #:modes premise syntax ( #16 )
2017-07-24 11:11:56 -04:00
Milo
61ad998c7a
simplified and documented linear language ( #15 )
2017-07-21 17:57:00 -04:00
Milo
e9c4b61db8
Added keyword in premises to allow parameterized call to infer ( #14 )
2017-07-21 15:04:50 -04:00
Alex Knauth
9d3c55d02b
add current-var-assign parameter ( #12 )
...
* add current-var-assign parameter
* add example of linear language + tests (Based on @iitalics work in pull request #11 )
2017-07-07 02:20:36 -04:00
AlexKnauth
7acbcbb0cc
add source location
2017-04-27 21:21:49 -07:00
AlexKnauth
e92156e78a
provide more pattern expanders for stlc+union base types
2017-04-25 16:47:11 -07:00
Alex Knauth
095c47c6cb
fix union collapsing ( #9 )
2017-04-25 13:35:47 -07:00
Alex Knauth
bbcdfaf9cf
add ~typecheck and ~⊢ pattern expanders ( #6 )
...
* add ~typecheck and ~⊢ pattern expanders
So that in normal macros, syntax classes, and normal syntax-parse
expressions, you can use use the Turnstile syntax to do typechecking
* add documentation for ~typecheck and ~⊢
2017-04-17 12:41:02 -07:00
AlexKnauth
f9199f6e37
Use filter-maximal for pruning redundant elements in unions
2017-04-10 21:41:15 -07:00
Milo Turner
2e03856589
Listed #:as keyword available in define-primop
2017-04-04 15:01:09 -04:00
Milo Turner
02fbf9f6d5
Listed the syntax class attributes for type-bind, type-ctx, type-ann
2017-04-04 15:01:09 -04:00
Milo Turner
881912d1fd
change some docs to adhere to the behavior of the code
2017-04-04 15:01:09 -04:00
AlexKnauth
33db7ad092
add missing syntax/loc
2017-04-03 15:15:19 -07:00
AlexKnauth
713eec89ea
provide ~True and ~False from stlc+union.rkt
2017-04-03 11:21:24 -07:00
Stephen Chang
d6012a7472
fix typo in stx-datum-equal? (from last commit)
2017-03-31 16:00:03 -04:00
Stephen Chang
28f6d782ec
generalize stx-member
2017-03-31 15:15:04 -04:00
Stephen Chang
7e3a21ba6f
extends form supports non-strs and allows explicit prefix
2017-03-30 19:01:56 -04:00
AlexKnauth
84b5a8759f
add stx-length>=? and stx-length<=?
2017-03-30 10:16:59 -07:00
Stephen Chang
28fa4dfb48
do not reprovide rackunit in rackunit-typechecking
2017-03-24 10:59:52 -04:00
Stephen Chang
2643d7c8f8
exclude rackunit-typechecking from compile
2017-03-23 16:38:54 -04:00
Stephen Chang
72bd18cd1a
exclude rackunit-typechecking from test
2017-03-23 16:23:35 -04:00
Stephen Chang
11551ee860
add turnstile/rackunit-typechecking abbrev
2017-03-23 15:43:34 -04:00
Stephen Chang
31c3bba5c9
add current-host-lang; fix reuse to work with non-strs
...
- other various stx conveniences
- provide more require/provide forms in default mod-beg
- fix tests and examples to work with current-host-lang
2017-03-22 17:04:48 -04:00
Stephen Chang
01799a12da
add with-ctx shorthand
2017-03-21 17:55:45 -04:00
Stephen Chang
3d9ef8424c
start dependent types example
2017-03-10 17:03:30 -05:00
Stephen Chang
0bccf822ad
type= handles literals
2017-03-06 13:21:49 -05:00
Stephen Chang
50f08886d1
rackunit-typechecking: add more esc chars
2017-03-03 16:20:16 -05:00
