Idris 2

Idris 2 is a dependently-typed functional programming language inheriting principally from Haskell and Agda. Idris is most focused on exploring software developed using dependent types, and is the least theorem-focused language of its kind.

Useful links

• Idris 2 user's guide

• Idris 2 package list

• API docs — base

• API docs — contrib

• Github — idris-lang/Idris2

Deriving interface instances

See Höck's library, elab-util.

  import Derive.Prelude
  %language ElabReflection
  record Positive where
    constructor MkPositive
    val : Nat
    0 prf : IsSucc val

  %runElab derive "Positive" [Show,Eq,Ord]