../ MakefileError message tinker15 years ago binary.idrMore sane scoping rules for where/type classes Parameters in the type signature get propagated, indices do not. So you no longer need to pass parameters explicitly if you need them in a where clause, and you no longer need to give explicitly typed helpers …14 years ago bmain.idrAdded :l and :m commands to REPL14 years ago btree.idrMade tutorial and examples consistent with latest library15 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.idrAdded :l and :m commands to REPL14 years ago idiom.idrMake 'Type' the type of types instead of Sets ...after mailing list discussion14 years ago interp.idrChanged approach to unification Instead of failing immediately, maintain a list of blocked problems and refine during elaboration.14 years ago letbind.idrMade tutorial and examples consistent with latest library15 years ago prims.idrRemove semicolons in tutorial15 years ago theorems.idrMake 'Type' the type of types instead of Sets ...after mailing list discussion14 years ago universe.idrMake 'Type' the type of types instead of Sets ...after mailing list discussion14 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.idrMake 'Type' the type of types instead of Sets ...after mailing list discussion14 years ago wheres.idrUpdate where type inference example in tutorial13 years ago