../ Vect/Don't reset totality for non-total things13 years ago Bits.idrRemove needless Prelude imports13 years ago BoundedList.idrRemove some of the more easily avoided %assert_totals13 years ago Buffer.idrMove buffer offset handling into idris code13 years ago Complex.idrRemove needless Prelude imports13 years ago Floats.idrRemove needless Prelude imports13 years ago Fun.idrRe-rename FunN all the way back to Fun.13 years ago HVect.idrMoved libraries around, removed 'effects' flag13 years ago Heap.idrReplace some Heap proofs with impossible.13 years ago Mod2.idrMoved libraries around, removed 'effects' flag13 years ago Morphisms.idrRemove needless Prelude imports13 years ago Rel.idrRe-rename FunN all the way back to Fun.13 years ago Sign.idrMoved libraries around, removed 'effects' flag13 years ago SortedMap.idrRemove needless Prelude imports13 years ago SortedSet.idrRemove needless Prelude imports13 years ago Vect.idrMoved libraries around, removed 'effects' flag13 years ago ZZ.idrRefactor parsing of bracketed expressions13 years ago