Add topic "Idris" Accepted
The requested resource couldn't be found.
Changes: 5
-
Add A Crash Course in Idris 2
- Title
-
- Unchanged
- A Crash Course in Idris 2
- Type
-
- Unchanged
- Article
- Created
-
- Unchanged
- 2020-05-20
- Description
-
- Unchanged
- This is a crash course in Idris 2 (sort of a tutorial, but rather less gentle I’m afraid!). It provides a brief introduction to programming in the Idris Language. It covers the core language features, assuming some experience with an existing functional programming language such as Haskell or OCaml.
- Link
-
- Unchanged
- https://idris2.readthedocs.io/en/latest/tutorial/index.html
- Identifier
-
- Unchanged
- no value
Resource | v1 | current (v1) -
Add Idris
- Title
-
- Unchanged
- Idris
- Description
-
- Unchanged
- Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but it is designed to be a general-purpose programming language similar to Haskell. The Idris type system is similar to Agda's, and proofs are similar to Coq's, including tactics (theorem proving functions/procedures) via elaborator reflection. Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages. Idris compiles to C (relying on a custom copying garbage collector using Cheney's algorithm) and JavaScript (both browser- and Node.js-based). There are third-party code generators for other platforms, including JVM, CIL, and LLVM.Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine.
- Link
-
- Unchanged
- https://en.wikipedia.org/?curid=39035048
Topic | v1 | current (v1) -
Add Idris treated in Type-driven development with Idris
- Current
- treated in
Topic to resource relation | v1 -
Add Idris has official A Crash Course in Idris 2
- Current
- has official
Topic to resource relation | v1 -
Add Programming language e.g. Idris
- Current
- e.g.
Topic to topic relation | v1