on 9302221 help sign in
Idris-dev/libs/prelude
2 folders, 5 files
../ Decidable/Reformulate decEq for Vect. Prelude/Add a few Stream functions Builtins.idrAllow second argument of assert_smaller to be of different type than first argument since this could be useful for functions that are written with Universe-style pattern matching, i.e., where the rhs pattern has different type than the lhs expression. IO.idrRemove prim_io_bind and prim_io_return from run__IO. MakefileFix .PHONY targets in Makefiles Prelude.idrMore docstrings prelude.ipkgAdd Uninhabited to Prelude