git.iko.soy/Idris-dev
on 10ea548 help sign in
history oftutorial/examples/binary.idr
all commits
628b851Added Cast to the prelude, and defined casts between primitivesEdwin Brady 8b1e498Change 'data' and where syntax so that they don't need '|' This breaks old code - instead ofEdwin Brady b0f47e1Made braces optional (at the expense of 'with' now needing the expression to be tested in brackets) do notation doesn't quite behave right - the first token after the do block must be at a lower level of indentation, which means putting it in brackets is awkward.Edwin Brady 2e9fcd4Remove semicolons in tutorialEdwin Brady ebf9100Binary adder exampleEdwin Brady