Apostolis Xekoukoulotakis

I added all the operators that malfunction supports.

3

I added all the operators that malfunction supports. Unfortunately, trying to use xor operator results in segmentation fault. ``` module Main import Data.Bits main : IO () main = do...

Debug *.js.dna files with sourcemaps

2

http://www.html5rocks.com/en/tutorials/developertools/sourcemaps/ Now, the only way seems to be to generate the rna file and debug that file.

vim - identation support

5

@mgor I was wondering if vim could help us indent the generated code. Having gg=G indent the file would be great.

Turn Γ into a parameter.

1

https://github.com/plfa/plfa.github.io/blame/dev/src/plfa/part2/DeBruijn.lagda.md#L783 In the Value definition, the context can be a parameter.

Replacing an undefined with a hole [here](https://github.com/xekoukou/learning_cubicaltt/blob/f5336256520e7d0b25c2bfab1250521d0498389e/lecture4.ctt#L52) results in a cubicaltt crash with error : ``` Hole at (52,46) in lecture4: A : U -------------------------------------------------------------------------------- (x : Sigma A (\(x...

Substitution in Tactic.Reflection.Subtitute is buggy

1

Consider this code : ```agda open import Agda.Builtin.Reflection open import Reflection open import Prelude.Nat open import Prelude.Bool open import Prelude.Unit open import Prelude.List open import Tactic.Reflection.Substitute fff : Term fff...

Triggers internal agda error.

2

https://github.com/agda/agda/issues/3805

``` test : Vect n a -> String test [] {n=Z} = case (Z) of Z => ?fdgf_1 (S k) => ?fdgf_2 test (x :: xs) {n=n} = ?test_rhs_2 ```...

Case splitting results in error message "Elaborating Builtins.Pair arg A: CantUnify False ....."

1

Trying to case split on `x` at the second case of the `belongs` function... ``` import Data.Vect data Node : String -> Type where MkNode : (s : String) ->...