Idris Programming Language

1–30 of 1681

0 selected

Attila Lendvai, Edwin Brady7

Jan 23

FTR, as part of this exploration, i have refactored the build system of Idris2, which is ready for

unread,

FTR, as part of this exploration, i have refactored the build system of Idris2, which is ready for

Jan 23

Jan 17

Written in Idris2: a demo of non-Euclidean geometry using WebGL

On Tue, Jan 18, 2022 at 04:43:44AM +0000, James Cook wrote: > I just published something I had a

unread,

Written in Idris2: a demo of non-Euclidean geometry using WebGL

On Tue, Jan 18, 2022 at 04:43:44AM +0000, James Cook wrote: > I just published something I had a

Jan 17

Jorge Gomez Abrante

Jan 16

Guile Code Generator

Hi, Is anyone working on a Guile Code Generator for Idris?

unread,

Guile Code Generator

Hi, Is anyone working on a Guile Code Generator for Idris?

Jan 16

mmhell...@gmail.com

Jan 2

Idris 2 0.5.1 for JVM

Hello everyone, I am happy to announce that Idris 2 JVM backend has finally caught up to Idris 2

unread,

Idris 2 0.5.1 for JVM

Hello everyone, I am happy to announce that Idris 2 JVM backend has finally caught up to Idris 2

Jan 2

apostolis.xe...@gmail.com, Nathan Ringo5

Jan 2

perceus reference counting - dependent types without a garbage collector?

Main_ones is a function that produces a stream of ones. You need to look at the memory as it is

unread,

perceus reference counting - dependent types without a garbage collector?

Main_ones is a function that produces a stream of ones. You need to look at the memory as it is

Jan 2

tony mailer, Denis Buzdalov3

12/31/21

Error about negative Nat

Ah, gotcha. Thanks for the detailed explanation. On Thursday, December 30, 2021 at 8:50:44 PM UTC-5

unread,

Error about negative Nat

Ah, gotcha. Thanks for the detailed explanation. On Thursday, December 30, 2021 at 8:50:44 PM UTC-5

12/31/21

12/28/21

Any way to speed up Data.Fin conversions, e.g. strengthen, fromInteger?

On the other hand, strengthen, fromInteger and finToInteger all seem to take O(n) time. Is there a

unread,

Any way to speed up Data.Fin conversions, e.g. strengthen, fromInteger?

On the other hand, strengthen, fromInteger and finToInteger all seem to take O(n) time. Is there a

12/28/21

Jan de Muijnck-Hughes, James Cook2

12/22/21

Community Announcements are also made on Discord...

> I have asked the admins for this Discord community to ensure that all > 'Community

unread,

Community Announcements are also made on Discord...

> I have asked the admins for this Discord community to ensure that all > 'Community

12/22/21

12/17/21

IJCAR 2022 - Call for Papers

IJCAR 2022 - Call for Papers https://easychair.org/smart-program/IJCAR2022/. ***Important Dates***

unread,

IJCAR 2022 - Call for Papers

IJCAR 2022 - Call for Papers https://easychair.org/smart-program/IJCAR2022/. ***Important Dates***

12/17/21

12/8/21

Certified Programs and Proofs (CPP) 2022: Call for Participation

*** Call for Participation *** *** Certified Programs and Proofs (CPP) 2022 *** - Early registration

unread,

Certified Programs and Proofs (CPP) 2022: Call for Participation

*** Call for Participation *** *** Certified Programs and Proofs (CPP) 2022 *** - Early registration

12/8/21

Wind R, Denis Buzdalov2

11/30/21

Trouble proving mult n 0 = 0

вт, 30 нояб. 2021 г. в 23:41, 'Wind R' via Idris Programming Language <idris-lang@

unread,

Trouble proving mult n 0 = 0

вт, 30 нояб. 2021 г. в 23:41, 'Wind R' via Idris Programming Language <idris-lang@

11/30/21

James Cook, … Denis Buzdalov22

10/8/21

Any way to work around Javascript stack size limit?

I'm finally getting back to this. After some experimentation, I think it's not actually the

unread,

Any way to work around Javascript stack size limit?

I'm finally getting back to this. After some experimentation, I think it's not actually the

10/8/21

10/7/21

post-doctoral research position - Effect Handler Oriented Programming - Edinburgh

Hi, I have an opening for a post-doctoral research position at The University of Edinburgh on Effect

unread,

post-doctoral research position - Effect Handler Oriented Programming - Edinburgh

Hi, I have an opening for a post-doctoral research position at The University of Edinburgh on Effect

10/7/21

Tornai, … Denis Buzdalov3

9/28/21

Enforcing a binary search tree ordering in the data type

`Ord` is particularly painful to work with in the proof-world setting. First, it has a lot of

unread,

Enforcing a binary search tree ordering in the data type

`Ord` is particularly painful to work with in the proof-world setting. First, it has a lot of

9/28/21

James Cook, … Denis Buzdalov10

9/26/21

Idris2: How to specify named implementation as input to default implementation?

Much better, thanks! Maybe I will continue to use it, since it's not too bad. On Monday, 27

unread,

Idris2: How to specify named implementation as input to default implementation?

Much better, thanks! Maybe I will continue to use it, since it's not too bad. On Monday, 27

9/26/21

9/18/21

Idris 2 version 0.5.0 released

Dear all, Idris 2 version 0.5.0 has been released. You can find full details, including all the

unread,

Idris 2 version 0.5.0 released

Dear all, Idris 2 version 0.5.0 has been released. You can find full details, including all the

9/18/21

9/8/21

30 months postdoctoral research position at University of Sheffield involving proof-assistant-based verification -- application deadline 23 Sept. 2021

Greetings, A postdoctoral research position (Grade 7) is available at the University of Sheffield.

unread,

30 months postdoctoral research position at University of Sheffield involving proof-assistant-based verification -- application deadline 23 Sept. 2021

Greetings, A postdoctoral research position (Grade 7) is available at the University of Sheffield.

9/8/21

9/6/21

Call for Contributions: WITS 2022

---------------------------------------------------------------------- CALL FOR CONTRIBUTIONS 1st

unread,

Call for Contributions: WITS 2022

---------------------------------------------------------------------- CALL FOR CONTRIBUTIONS 1st

9/6/21

9/2/21

Totality checker behaving strangely when making changes to Prelude

I managed to reproduce the below outside of Prelude, and filed issue #1896. On Saturday, 28 August

unread,

Totality checker behaving strangely when making changes to Prelude

I managed to reproduce the below outside of Prelude, and filed issue #1896. On Saturday, 28 August

9/2/21

8/19/21

Certified Programs and Proofs (CPP) 2022: Final Call for Papers

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical

unread,

Certified Programs and Proofs (CPP) 2022: Final Call for Papers

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical

8/19/21

Ashwin Bhaskar, alru...@gmail.com2

8/1/21

How to concat a string and a char in idris?

Despite the apparent convenience, :let e1 : String = "123" does not define variable e1 to

unread,

How to concat a string and a char in idris?

Despite the apparent convenience, :let e1 : String = "123" does not define variable e1 to

8/1/21

Jan de Muijnck-Hughes

7/26/21

Merging Idris-Hackers into Idris-Community.

Dear Idris Community. With the rise of Idris2 we have seen some nice advancements in the community.

unread,

Merging Idris-Hackers into Idris-Community.

Dear Idris Community. With the rise of Idris2 we have seen some nice advancements in the community.

7/26/21

mmhell...@gmail.com

7/20/21

[Announce] Idris 2 - 0.2.1 release for the JVM

Hello all, I am happy to announce the intial version for Idris 2 - 0.2.1 on the JVM. This is compiled

unread,

[Announce] Idris 2 - 0.2.1 release for the JVM

Hello all, I am happy to announce the intial version for Idris 2 - 0.2.1 on the JVM. This is compiled

7/20/21

6/23/21

Idris 2 version 0.4.0 released

Dear all, Idris 2 version 0.4.0 has been released. You can find full details, including all the

unread,

Idris 2 version 0.4.0 released

Dear all, Idris 2 version 0.4.0 has been released. You can find full details, including all the

6/23/21

6/18/21

Lectureships in St Andrews

Hi all, We're hiring lecturers (and senior lecturers and readers) in St Andrews, and it'd be

unread,

Lectureships in St Andrews

Hi all, We're hiring lecturers (and senior lecturers and readers) in St Andrews, and it'd be

6/18/21

6/14/21

Call for Papers: Fifth Workshop on Formal Mathematics for Mathematicians (FMM 2021)

========================================================= Call for Papers Fifth Workshop on Formal

unread,

Call for Papers: Fifth Workshop on Formal Mathematics for Mathematicians (FMM 2021)

========================================================= Call for Papers Fifth Workshop on Formal

6/14/21

6/14/21

Certified Programs and Proofs (CPP) 2022: Call for Papers

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical

unread,

Certified Programs and Proofs (CPP) 2022: Call for Papers

Certified Programs and Proofs (CPP) is an international conference on practical and theoretical

6/14/21

xp xp, … mukesh tiwari5

6/12/21

Dependent type List

Thanks Mukesh, that's interesting. xp On Sat, 12 Jun 2021 at 23:48, mukesh tiwari <

unread,

Dependent type List

Thanks Mukesh, that's interesting. xp On Sat, 12 Jun 2021 at 23:48, mukesh tiwari <

6/12/21

Corvo Liu, Ohad Kammar2

6/12/21

Why we have to provide proofs in order to let patterns match twice?

Because pattern matching is about matching data constructors, and in this definition you are not

unread,

Why we have to provide proofs in order to let patterns match twice?

Because pattern matching is about matching data constructors, and in this definition you are not

6/12/21

Corvo Liu, art yerkes3

6/6/21

How to use constants in Idris2?

Thanks a lot! 在2021年6月7日星期一 UTC+8 上午12:52:15<art.y...@gmail.com> 写道： I don't think idris

unread,

How to use constants in Idris2?

Thanks a lot! 在2021年6月7日星期一 UTC+8 上午12:52:15<art.y...@gmail.com> 写道： I don't think idris

6/6/21

Search

Clear search

Close search

Google apps

Main menu