git.iko.soy/Idris-dev
on da674d3 help sign in
history oftutorial/examples/views.idr
all commits
b752e2dMade tutorial and examples consistent with latest libraryEdwin 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 dcc09e0Fix metavariable naming in namespacesEdwin Brady