Commit Graph

8 Commits

Author SHA1 Message Date
Brian Huffman
ca1dd23173 Fix error in examples/AE.cry.
The error was: "built-in type 'Integer' shadowed in type synonym"
2018-07-19 09:31:46 -07:00
Iavor Diatchki
920cb58ad0 Some cleanup and doubt that I've enconded the algorithm correctly 2017-09-27 09:50:47 -07:00
Iavor Diatchki
b8707033d7 Add module parameters as extra vars---prints nicer error messages. 2017-09-26 15:29:23 -07:00
Iavor Diatchki
83d0132e50 Add module-level constraints to assumptions when proving implications. 2017-09-26 15:21:40 -07:00
Iavor Diatchki
ccc4b828c2 Represent type parameters as just type variables. 2017-09-25 11:41:00 -07:00
Iavor S. Diatchki
d1abac0cec Update design; handle numeric type parameters in type checking SMT 2017-09-21 14:57:53 -07:00
Iavor Diatchki
f7e1a941e2 checkpoint 2017-09-21 09:28:01 -07:00
Iavor Diatchki
9f2a2ac3a4 Incomplete example of using 'abstract' types. 2017-09-19 14:28:08 -07:00