Idris2

Idris2 copied to clipboard

Double IEEE constants: infinity, NaN, epsilon ... where are they?

6

**Issue by [nicolabotta](https://github.com/nicolabotta)** _Tuesday Oct 29, 2019 at 07:48 GMT_ _Originally opened as https://github.com/edwinb/Idris2-boot/issues/146_ ---- Is there a way of accessing these values in Idris 2? Something like `Numeric.IEEE`in Haskell?...

edwinb

"${HOLE NAME} is already defined" in `with`

1

``` data Name : Type where UN : String -> Name -- user written name MN : String -> Int -> Name -- machine generated name data IsVar : Name...

gergoerdi

Normalization of Field Projections Rough Edge

1

Seems like the compiler doesn't expand field projections of records unless they are explicitly deconstructed. # Minimal Example ``` public export record SimpleRecord where constructor MkSimpleRecord simpleField : Bool public...

fabianhjr

Linear arguments and with clauses don't mix well

3

The compiler seems conflicted whether it would like linear arguments to be used in `with` clauses or not. ```idris pair : (1 _ : a) -> b -> (a, b)...

mb64

unhelpful error message while unifying identical types

7

I get a cryptic error message while lifting a `Preorder` relationship to `Maybe`. The type-checker is unable to unify identical types. # Steps to Reproduce Using the definition of `Preorder`...

rgrover

Version: 0.2.0 OS: Windows using WSL Changed `PREFIX` to `/usr/local` and installed. Works fine while under `root`/`sudo` shell, or using `sudo idris2`, but shows `Uncaught error: (implicit):1:1--1:1:Prelude not found` on...

bascott

Name clash when using implicit function type

1

# Steps to Reproduce ``` import Data.List.Elem %default total Subset : List a -> List a -> Type Subset xs ys = {0 x : a} -> Elem x xs...

clayrat

Confusing error message when making instances for nested indexed structures

1

# Steps to Reproduce ``` data Thin : List a -> List a -> Type where Nil : Thin [] [] Skip : Thin xs ys -> Thin xs (y::ys)...

clayrat

Error message is unclear when Elab script references unimported names

3

Not a big deal, but the problem here is that `C` doesn't import `A`, so when it evals the `Elab` in `B`, (which returns an elab script that does reference...

redfish64

Order of `-p` libraries are important.

1

I experiment with idris2 custom code generation backend, and it seems that the order `-p` arguments are important for the compilation result. ``` euler% idris2 -p contrib -p network -p...

andorp