search

joelburget / lvca

language verification, construction, and analysis
https://lvca.dev
MIT License
20 stars 0 forks source link

Kind annotations #15

Closed joelburget closed 3 years ago

joelburget commented 3 years ago

I'm working on adding kind checking. One thing I don't think I'll get to right now, but would be nice, is optional kind annotations for sorts in abstract syntax declarations. I'd like to enable them both at the top level and when declaring an argument to a newly-defined sort. Example:

primitive : *
list : * -> *

foo (a : *) := foo(list a)
bar b := bar(b primitive) // note that annotations are still optional, `b : * -> *` is inferred.
joelburget commented 3 years ago

Added in 57387edcb9f4ace5bf7b9401105ac213b2b37e81 and 0f56a808aee599c11a0ec065bc66f2d114d8368e