Skip to main content
Back to top
Ctrl
+
K
A Crash Course in Idris 2
Introduction
Getting Started
Prerequisites for Windows
Types and Functions
Interfaces
Modules and Namespaces
Multiplicities
Packages
Example: The Well-Typed Interpreter
Views and the “
with
” rule
Theorem Proving
Interactive Editing
Miscellany
Further Reading
Frequently Asked Questions
Compiling to Executables
Incremental Code Generation
Chez Scheme Code Generator
Racket Code Generator
Gambit Scheme Code Generator
Javascript and Node Code Generators
C with Reference Counting
Building Idris 2 with new backends
Custom backend cookbook
Libraries
Changes since Idris 1
Type Driven Development with Idris: Updates Required
Packages
Where To Find Libraries
Structuring Idris 2 Applications
Introducing App
Exceptions and State
Defining Interfaces
Linear Resources
Foreign Function Interface
FFI Overview
Example: Minimal Readline Bindings
Theorem Proving
Propositions and Judgments
Running example: Addition of Natural Numbers
Inductive Proofs
Pattern Matching Proofs
Proving Propositional Equality
Implementation Notes
Implementation Overview
The IDE Protocol
Idris2 Reference Guide
Packages
Documenting Idris Code
Environment Variables
Dot syntax for records
Literate Programming
Overloaded literals
Operators
String literals in Idris
Pragmas
Builtins
Debugging The Compiler
Failing blocks
Cookbook
Parsing
Search
Error
Please activate JavaScript to enable the search functionality.
Ctrl
+
K
