Idris2

Idris2 copied to clipboard

demo of #3355

andrevidela

Layout processing - same column ; Haskell vs Idris

2

# Steps to Reproduce The following code is accepted in Idris2 ```haskell t : Int t = let z = 1000 in 1 ``` but the following code is not...

MilanKral

# Problem If we define a type inside a namespace and it's not publicly exported, then we shouldn't be able to pattern match over its definition. This works fine, as...

JavierGelatti

Totality checker inconsistency when using Inf

2

# Problem Sometimes the totality checker validates a function as total when it's not. In particular, this happens when using `Inf` in the return type, combined with having the recursive...

JavierGelatti

# Steps to Reproduce ```Idris %macro getTTImp : v -> Elab TTImp getTTImp v = quote v u1 = getFC $ getTTImp ('a' == 'b') -- this has physicalIdrSrc u2...

freddi301

Bootstrap with Racket error: `raco: Unrecognized command: exe`

3

For the sake of testing I tried to build `idris2` with `racket` instead of `chez-scheme`. It failed with the following: ``` cp support/c/libidris2_support.dylib bootstrap-build/idris2_app/ sed 's|__PREFIX__|/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_lang_idris2/idris2/work/Idris2-0.7.0/bootstrap-build|g' \ bootstrap/idris2_app/idris2.rkt \ >...

barracuda156