Apostolis Xekoukoulotakis
Apostolis Xekoukoulotakis
As soon as I have the time, I will try to update this to the new syntax.
There are remaining problems in this pull request. 1. Fixed length integers are treated as unsigned in Idris. 2. The shift operators in Idris does not take 'int' in the...
I am putting this as a future goal. I haven't looked at it very closely. The way to debug node-javascript is to use the browser debugger (like chrome debugger). Chrome...
My bad.I said it wrong. I want to be able to indent the original file, the .dna file,but the parts that go to the output. ``` .if (a
For example, your mergesort implementation does not work anymore. https://twitter.com/ulfnorell/status/727543430335873028
Completely untested , this might work : ```agda module Substitute where open import Prelude hiding (abs) open import Builtin.Reflection open import Tactic.Reflection.DeBruijn patternArgsVars : List (Arg Pattern) → Nat patternVars...
I am on the process of learning about SIP. Maybe a good candidate is the final coalgebra as a structure? https://github.com/niccoloveltri/final-pfin
To transport the structure of CommRIng from one Int into the other, one needs to reorganize the CommRingStr, split the raw structure from the Propositions : https://github.com/agda/cubical/pull/552 I will give...
It would be nice to see latency variance as well.
For Debian, it requires libbsd-dev.