Idris2

Idris2 copied to clipboard

Unification tries to unify irrelevant things and fails to do so

1

# Steps to Reproduce This is a shrunk from a real code, so it lacks practicality, but still reveals strange behaviour. Consider the following definitions: ```idris data E = MkE...

buzden

idris2 generates invalid scheme

1

# Steps to Reproduce Loading my records library in the repl: https://gist.github.com/kuribas/36291152663166bb1ee4b1eca7d6337f Then printing my testx record using :exec ``` :exec print testx ``` # Expected Behavior It should print...

kuribas

# Steps to Reproduce Consider two variants of the same function: ```idris f : (n : Nat) -> (Void, Void) -> Nat f 0 (_, _) impossible f 1 (_,...

buzden

Quantity is lost when matching on a lazy value

3

`Lazy` values can be matched using `Delay`. But when `Lazy` value has unrestricted quantity, matched under `Delay` must have the same quantity. This usually holds, but when a value holding...

buzden

Incorrect elaboration of lambda-case within a parameters block

4

# Steps to Reproduce ```idris -- Works Fine : Unit -> Nat Fine = \case () => 0 data Good : Type where AGood : Good Works : Good ->...

ohad

# Steps to Reproduce ```idris public export Hmmm : Nat {- -}-} ``` # Expected Behavior Report a parse error on the final `-}` on the final line. ``` --...

ohad

[ RFC ] Process for moving modules out of the `contrib` package.

10

UPDATES (not part of proposal text): 1. 2023-02-25 - The license requirement description for third party derivative work was updated based on RFC comments. ---- ## Summary / Motivation A...

mattpolzin

# Environment System: Ubuntu 2022 on Win10 WSL idris: Idris 2, version 0.6.0-fd217722b # Steps to Reproduce test.idr ``` record Comp (f,g : Type -> Type) (a : Type) where...

fonqL

[ docs ] Build IdrisDoc in a namespace.

4

When invoking `idris2 --mkdocs foobar.ipkg`, the current behaviour is for the compiler to dump the documentation in `${builddir}/docs`. The location `${builddir}/docs` is used regardless of the package name. Thus for...

jfdm

# Description The PR enhances totality checking to see size changes underneath matching constructors, addressing issue #3317. With this change Idris recognizes: - `Just xs` is smaller than `Just (x...

dunhamsteve