Idris Programming Language

1–30 of 1671

0 selected

James Cook, … Denis Buzdalov22

Oct 8

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

Oct 8

Oct 7

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

Oct 7

Tornai, … Denis Buzdalov3

Sep 28

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

Sep 28

James Cook, … Denis Buzdalov10

Sep 26

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

Sep 26

Attila Lendvai, Edwin Brady6

Sep 20

i have finally understood the issue. benefits: it's much easier to work out some bootstrap issues

unread,

i have finally understood the issue. benefits: it's much easier to work out some bootstrap issues

Sep 20

Sep 18

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

Sep 18

Sep 8

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.

Sep 8

Sep 6

Call for Contributions: WITS 2022

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

unread,

Call for Contributions: WITS 2022

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

Sep 6

Sep 2

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

Sep 2

Aug 19

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

Aug 19

Ashwin Bhaskar, alru...@gmail.com2

Aug 1

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

Aug 1

Jan de Muijnck-Hughes

Jul 26

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.

Jul 26

mmhell...@gmail.com

Jul 20

[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

Jul 20

Jun 23

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

Jun 23

Jun 18

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

Jun 18

Jun 14

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

Jun 14

Jun 14

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

Jun 14

xp xp, … mukesh tiwari5

Jun 12

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 <

Jun 12

Corvo Liu, Ohad Kammar2

Jun 12

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

Jun 12

Corvo Liu, art yerkes3

Jun 6

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

Jun 6

scott....@gmail.com, … Robert Watson7

Jun 2

Trouble proving that 2 does not divide 1

My original terminology was wrong. Jake's clarification is clear. The fundamental concept of

unread,

Trouble proving that 2 does not divide 1

My original terminology was wrong. Jake's clarification is clear. The fundamental concept of

Jun 2

Nathan Ringo, Edwin Brady3

May 30

Creating libraries for other languages

Okay, for posterity's sake (does this mailing list get indexed by search engines?), I got this

unread,

Creating libraries for other languages

Okay, for posterity's sake (does this mailing list get indexed by search engines?), I got this

May 30

Italo Waddington, Stefan Höck5

May 28

Newbie in Idris

Never mind, I will install Ubuntu in a virtual machine and then install Idris 2, it will be easier.

unread,

Newbie in Idris

Never mind, I will install Ubuntu in a virtual machine and then install Idris 2, it will be easier.

May 28

May 26

PhD position on the formalization of logical calculi in Saarbrücken

A PhD position is open at the MPI for Informatics in Saarbrücken, supervised by Christoph Weidenbach,

unread,

PhD position on the formalization of logical calculi in Saarbrücken

A PhD position is open at the MPI for Informatics in Saarbrücken, supervised by Christoph Weidenbach,

May 26

Ashwin Bhaskar, alru...@gmail.com2

May 23

Idris can't disambiguate between Vect.:: and List.::

Your syntax for qualifying operator names is a bit off. In order to refer to Vect's cons, (Data.

unread,

Idris can't disambiguate between Vect.:: and List.::

Your syntax for qualifying operator names is a bit off. In order to refer to Vect's cons, (Data.

May 23

Jan de Muijnck-Hughes, … Ohad Kammar12

May 22

What are we to do about Idris2 and Emacs support?

Dear Nicholas, There's a fork mode: https://github.com/redfish64/idris2-mode which works OK at

unread,

What are we to do about Idris2 and Emacs support?

Dear Nicholas, There's a fork mode: https://github.com/redfish64/idris2-mode which works OK at

May 22

Daniel Gavrila, Ohad Kammar3

May 19

Dear Ohad, many thanks for your detailed advice. I will see how far can I go ... Best regards, Daniel

unread,

Dear Ohad, many thanks for your detailed advice. I will see how far can I go ... Best regards, Daniel

May 19

May 19

Position of Lecturer or Senior Lecturer in Cybersecurity at University of Sheffield

Greetings, The Department of Computer Science at University of Sheffield has an open position of

unread,

Position of Lecturer or Senior Lecturer in Cybersecurity at University of Sheffield

Greetings, The Department of Computer Science at University of Sheffield has an open position of

May 19

Corvo Liu, … alru...@gmail.com4

May 18

Why Idris don't have guards?

Not to detract from the cool dependent-type stuff you can do with views, but the with syntax will let

unread,

Why Idris don't have guards?

Not to detract from the cool dependent-type stuff you can do with views, but the with syntax will let

May 18

Siyu Liu, art yerkes3

May 17

Is there a better way to write the following codes(eliminate nested cases)?

Thanks a lot! Corvo 在2021年5月17日星期一 UTC+8 下午1:30:01<art.y...@gmail.com> 写道： the mixing of status

unread,

Is there a better way to write the following codes(eliminate nested cases)?

Thanks a lot! Corvo 在2021年5月17日星期一 UTC+8 下午1:30:01<art.y...@gmail.com> 写道： the mixing of status

May 17

Search

Clear search

Close search

Google apps

Main menu