Ambroise
Ambroise
Currently, ` match%sedlex lexbuf with | "ρ" -> .. ` does not match, although ` match%sedlex lexbuf with | math -> if Sedlexing.Utf8.lexeme lexbuf = "ρ" then .. ` does....
Representations of types should be in one-to-one correspondance with C types for the put lemmas to be right. Thus they should contain the field names for records.
This PR implements the shallow embedding of ArrayPut, which is enough to compile the shallow embedding the led driver.. This PR also implements the shallow embedding of ArrayTake, but it...
The sum constructor of uval (in ML) only needs a list of booleans (indicating whether each constructor is checked) rather than the full list of the types of the constructors....
Consider the simple cogent program ``` type U7 main : U7 -> U7 main a = a ``` If I prepend the generated C file with `typedef struct U7 {...
``` type Example = {ptr : U8} type Example2 = { ptr2 : U8} main : (Example, Example2) -> (Example, Example2) main (r {ptr}, r2 {ptr2}) = (r { ptr...
Cogent fails to compile this function, on master: ``` main : all (l :~ {a : U8} ). {a : U8} layout l -> {a : U8} layout l main...
**Describe the bug** Coq-lsp doesn't work when the filename includes a dash. **To Reproduce** Steps to reproduce the behavior: 1. Insert a dash in the name of a working Coq...
The extension does not work if the workspace includes a file elm.js (tested on windows) ## Expected Behavior I should be able to use the extension features (e.g., ctrl+click on...
The ratio between the normal font size and the scriptstyle font size differs from standard LaTeX 1) In Latex (the second line is script style)  2) Same code in...