cogent
cogent copied to clipboard
au-ts
Cogent Project
In a nutshell, defaulting implicit offset to `after` is not compatible with layout polymorphism. One concrete example is: ``` type PairBool = { a : Bool, b : Bool }...
This commit fixes the declaration of the uabsfuns, i.e. the xi_0 and xi_1 terms in the corres theorems. These are now declared as Isabelle constants, which users can overload later...
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.
currently for `type B = { f1: #{ f1: U8, f2: U8 }, f2: U16 } layout record { f1: default, f2: 2B after f1 }`, it will generate `record...
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....
Currently, CI cycle times are awful --- and *really* variable. The longest recent build I've seen is 9h45m21s, and most builds hover between 5h and 9h. Occasionally, the caches will...
Aiming to make isa-parser usable as a Isabelle language parser
this PR substantially expands the Cogent documentation. the result is in two parts: - *An Introduction to Cogent*, largely based on introductory text that already existed; and - *Cogent Reference...
Consider the simple cogent program ``` type U7 main : U7 -> U7 main a = a ``` If I prepend the generated C file with `typedef struct U7 {...