Ohad Kammar
Ohad Kammar
# Steps to Reproduce ```idris $ cat Mutual.idr module Mutual private data Foo : Type public export data Foo : Type where ------------------------------ $ cat Import.idr import Mutual x :...
# Steps to Reproduce ```idris versionA : Bool -> Nat -> Nat versionA True k0 = k0 versionA False k0 = 0 versionB : Bool -> Nat -> Nat versionB...
# Steps to Reproduce ```idris import Data.Vect Bar : Vect n Type -> Type Bar [] = Int Bar (a :: rest) = a -> Bar rest Ex1 : Bar...
# Steps to Reproduce ```idris -- Works Fine : Unit -> Nat Fine = \case () => 0 data Good : Type where AGood : Good Works : Good ->...
# Steps to Reproduce ```idris public export Hmmm : Nat {- -}-} ``` # Expected Behavior Report a parse error on the final `-}` on the final line. ``` --...
I spotted a potential room for a little optimisation. Need to profile benchmark to see if performance improves a little. We already know which predicate we need to use to...
(the identity and the constant functors are normal). We did cover this in the lecture, but there is no trace for it in the notes, and this is later referenced.
Have a look at the introduction to Ken Shan's [a static simulation of dynamic delimited control](http://link.springer.com/article/10.1007%2Fs10990-007-9010-4). He lists lots of cool uses of delimited control: - backtracking search [references 11,...
Do you think you could implement [transparent code migration](http://www.cl.cam.ac.uk/~ok259/teaching/partII.html)?