Gunnar Teege

Isabelle C-Parser refuses to handle string literals.

1

When a Cogent program `stringconst.cogent` such as ``` f : String -> () g: () -> () g () = f "abc" ``` is compiled to C and loaded in...

Variable of unboxed abstract type is treated as linear.

3

``` type A type B a f : #(B A) -> () f b = () ``` causes the error message: ``` Parsing... Resolving dependencies... Typechecking... Desugaring and typing... Internal...

Defined constants cannot be used in lambda expressions. The docs say "no free variables", but is it really intended that this also applies to toplevel defined constants? Example: ``` c...

impossible happened when desugaring

1

The compiler asked me to report this... When compiling the following cogent source with cogent -g [pattern.txt](https://github.com/NICTA/cogent/files/2596180/pattern.txt) the compiler output was [log.txt](https://github.com/NICTA/cogent/files/2596154/log.txt)

And one more. When compiling `lv: U8 -> U8` `lv = \x => x+1` the compiler output was [log2.txt](https://github.com/NICTA/cogent/files/2596220/log2.txt)