Zilin Chen
Zilin Chen
**Comment by [ahixon](https://github.csiro.au/ahixon)** _Tue Jun 16 14:58:37 2015_ ---- Would also be interesting to benchmark a version that doesn't pass ExState around, at all (ie implicit environment/heap state). Should definitely...
**Comment by [lim060](https://github.csiro.au/lim060)** _Wed Dec 9 09:51:11 2015_ ---- We can't always translate this to the desired && in C, because the right operand could (and in this case, will)...
sort of a duplicate of #49.
We don't evaluate them. We instead substitute the variable with the RHS of `=`. So when they're mistakenly not constants, we don't handle it properly in the code generator.
I also think this could be potentially problematic if we had a proper refinement type system. ``` a : Int a = 5 ``` should probably be compiled to ```...
You need to download autocorres from http://ts.data61.csiro.au/projects/TS/autocorres/ and set `$AC_DIR` to it. The README files (https://github.com/NICTA/cogent#proofs) and the documentation (https://cogent.readthedocs.io/en/latest/verification.html?highlight=AC_DIR#building-running-the-generated-files) are not super clear about it; I'll fix it. Thanks...
even smaller example: ``` type A array_bget : all x. (A!, U32) -> x type Ra = #{ x : A, b : Bool } type L_p = < L_p_4...
@liamoc seems that minigent has the same issue: ``` f : A! -> Bool; g : { x : A, b : Bool }# -> { x : A, b...
no, but it doesn't reject the program.
Ok, but what about the fact that `r` is double-used in the put-expression?