Idris2-boot/libs/base/base.ipkg

package base

modules = Control.WellFounded,

          Data.Buffer,
          Data.Fin,
          Data.List,
          Data.List.Views,
          Data.Maybe,
          Data.Nat,
          Data.Nat.Views,
          Data.IORef,
          Data.So,
          Data.Strings,
          Data.Vect,
          
          Decidable.Equality,

          System,
          System.Concurrency.Raw,
          System.File,
          System.REPL
Add 'base' libraries 2019-06-15 13:54:22 +03:00			`package base`

			`modules = Control.WellFounded,`

			`Data.Buffer,`
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway). 2019-07-01 01:54:50 +03:00			`Data.Fin,`
Improve 'with' implementation Now supports with applications on the RHS when auto implicits are involved. Auto implicit bound names in patterns now become searches on the rhs in a with-application (I should write this construct up properly in a paper some time!) 2019-07-08 13:55:55 +03:00			`Data.List,`
			`Data.List.Views,`
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway). 2019-07-01 01:54:50 +03:00			`Data.Maybe,`
Add 'base' libraries 2019-06-15 13:54:22 +03:00			`Data.Nat,`
Improve 'with' implementation Now supports with applications on the RHS when auto implicits are involved. Auto implicit bound names in patterns now become searches on the rhs in a with-application (I should write this construct up properly in a paper some time!) 2019-07-08 13:55:55 +03:00			`Data.Nat.Views,`
Add 'base' libraries 2019-06-15 13:54:22 +03:00			`Data.IORef,`
Parse pattern matching lambda This is now enough for Chapter 5 tests to work 2019-07-03 15:04:25 +03:00			`Data.So,`
Add 'base' libraries 2019-06-15 13:54:22 +03:00			`Data.Strings,`
Make a start on Data.Vect 2019-06-30 19:38:40 +03:00			`Data.Vect,`
More base libraries This has shown up a problem with 'case' which is hard to fix - since it works by generating a function with the appropriate type, it's hard to ensure that let bindings computational behaviour is propagated while maintaining appropriate dependencies between arguments and keeping the let so that it only evaluates once. So, I've disabled the computational behaviour of 'let' inside case blocks. I hope this isn't a big inconvenience (there are workarounds if it's ever needed, anyway). 2019-07-01 01:54:50 +03:00
			`Decidable.Equality,`
Add 'base' libraries 2019-06-15 13:54:22 +03:00
			`System,`
			`System.Concurrency.Raw,`
Start adding tests for TypeDD book Also detailing any changes needed to the code. Added primitives for Doubles, and repl/replWith to get Chapter 2 code to work. 2019-06-30 17:50:58 +03:00			`System.File,`
			`System.REPL`
Add 'base' libraries 2019-06-15 13:54:22 +03:00