cooltt
cooltt copied to clipboard
RedPRL
😎TT
We should have something like ```ocaml type 'a pattern val match_tp : D.tp -> 'a pattern -> 'a m ``` An example would be something like: ```ocaml let* base, fam...
Relevant documentation: https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions # Errors, warnings, and notices We can output messages in a format that GitHub Actions understands. For example, output ``` ::warning file=test/a.cooltt,line=3,endLine=4,title=taste it::your Ch'i is critically low...
When messing around with some ideas that @cangiuli had regarding records, I came across the following crash: ```cooltt import prelude import hlevel -- Equivalences. def fiber (A : type) (B...
Right now the boundary sensitive refinement via extension types only works for negative types. In particular we can reduce `(M,N) : A * B [phi -> U]` to `M :...
I noticed a bug in the handling of pushing a substitution under a BindSym. Who else can see it? 🤦🏻♂️🤣 (Btw only saw this using 🧠, didn’t find an error...
## Basic Design + Syntax The (rough) syntax for defining an inductive type is as follows: ``` data type-name (x1 : p1) (x2 : p2) ... : (y1 : i1)...
(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...
There is no real pretty-printing of symbols without an environment.