@andrasKovacs6 Hey, I was wondering if you had any thoughts about how I might implement a validator for my core syntax, given the presence of metavariables? Eg. https://github.com/brendanzab/rust-nbe-for-mltt/blob/752f0fe6d2973ec5e1c138796915c6d08b40e14c/crates/mltt-core/src/validate.rs#L436-L440 … - ie. my solutions are value in the meta environment, but I can't get the type of those…
-
-
As an interested amateur I tried to understand the theory of this topic, but could not find literature. The small amount that i found [McBride] is understandable only for professional type theorists. Please consider writing an article or giving a talk for Haskellers.
-
What in particular were you interested in learning about?
- 5 more replies
New conversation -
-
-
I hoped to use a McBride-style shifting operator - it seems like it could be nice without being too tricky impl wise (NbE not withstanding). The annoying thing is that it seems I'd probably only need this universe level unification for validating my elaborated syntax…
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.