Carlo Angiuli
Carlo Angiuli
See, for example, what @favonia did in redtt.
(from a discussion with @favonia and @TOTBWF) We often define operations on paths (such as `symm`) by composition/coercion to `0` or `1`, but as soon as we want to prove...
The goal of this proposal, developed with @jonsterling, is to make `hcom` less unwieldy in practice. Comments are very welcome. The basic idea is to add a new `abstract-hcom A...
Top-level things don't have source locations; we need to add source locations to the metalanguage operations. A simple example is that `Print Foo.` will result in: ``` [Unknown Location] [Error]:...
e.g., "HaskellKanren is strongly-typed...It relies on Haskell's built-in type-checking to reject mistyped programs." I'm not sure how to patch the last two paragraphs of About to be correct, so I'm...
e.g., Text.PrettyPrint, to avoid the horrible concatenation that's going on.