../ MakefileFix error recovery in repl15 years ago binary.idrAdded Cast to the prelude, and defined casts between primitives15 years ago bmain.idrMade 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 a…15 years ago btree.idrRemove semicolons in tutorial15 years ago classes.idrMade 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 a…15 years ago foo.idrMade 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 a…15 years ago hello.idrRemove semicolons in tutorial15 years ago interp.idrAdded Cast to the prelude, and defined casts between primitives15 years ago letbind.idrMade 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 a…15 years ago prims.idrRemove semicolons in tutorial15 years ago theorems.idrRemove semicolons in tutorial15 years ago universe.idrNote on cumulativity in tutorial15 years ago usefultypes.idrChange 'data' and where syntax so that they don't need '|' This breaks old code - instead of15 years ago vbroken.idrRemove semicolons in tutorial15 years ago views.idrChange 'data' and where syntax so that they don't need '|' This breaks old code - instead of15 years ago