André Videla
André Videla
Sorry I just saw this. I just bought a computer with 32Gb of ram. … Just kidding, maybe you can have better chances by compling every file separately from the...
I don't think so, but maybe we could make an official release with the library precompiled
In order to keep the name of the namespace consistent and expressive, I propose we place this function in a module `Basics.Dependent` in `base. How does that sound?
`Basics` contains all the combinators on functions that we expect from a functional programming language, in particular it contains both `cong` and `flip` https://github.com/idris-lang/Idris2/blob/main/libs/prelude/Prelude/Basics.idr Importing a dependent version of it...
@Russoul @gallais @joelberkeley any feedback or ideas about `Basics.Dependent` in `base`?
> is this specific to `Basics`? Or is this just a consequence of being in `Prelude`? It is a consequence of being in `Prelude`
The goal of `prelude` is to be as small as possible. `dflip` hasn't been something that's been asked for before so there is little reason to conclude it needs to...
To remain consistent with #2456 We should place this in the same spot. I proposed `Basics.Dependent`, I suggest you chime in the thread to tell us what you think of...
That would be fine but then what would be the namespace for #2456?
Are we putting this in `Basics.Dependent`? @gallais @joelberkeley