Idris2

Idris2 copied to clipboard

[RefC] Add 16 and 32 bit access to base/Data.Buffer .

2

Some FFI definitions are missing in base/Data.Buffer. This PR adds 16 and 32 bit access routines.

seagull-kamome

Related to #2607 (doesn't solve it due to warnings not being emitted when errors are)

Z-snails

Prior to this PR, case splitting on an auto-implicit in a function clause resulted in invalid Idris syntax. _Before case split:_ ```idris test : Bool => () test @{x} =...

mattpolzin

Issue 2513 - handle erased, irrefutable lets

16

This PR addresses #2513 by adding a rig to ICase. It includes a test case named `idris2/linear016`. It needs to be double checked by someone familiar with elaboration of case...

dunhamsteve

Some compiler errors seem to have "Error" printed twice before the error description when used in custom backends. # Steps to Reproduce 1. Create the following file: ```idris import Compiler.Common...

magnostherobot

seagull-kamome

[RefC] add missing symbols of showcCleanStringChar

2

Compiler.RefC.Refc.showcCleanStringChar forgot some symbols. This PR fixes that and avoids the compiler error.

seagull-kamome

Implicit lambda arguments

10

**Issue by [clayrat](https://github.com/clayrat)** _Sunday Jul 28, 2019 at 00:28 GMT_ _Originally opened as https://github.com/edwinb/Idris2-boot/issues/56_ ---- (This is more of a feature request, but it's been a long-standing stumbling block for...

edwinb

Trans deps v3

5

See #2496 and #2469 pinging @stefan-hoeck

Z-snails

Javascript backend emitted code that access global variable

6

If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example...

iacore