Deriving facility for Idris

Deriving statement implemented in Elab . You can derive some interfaces for datatypes by %runElab derive [deriveName, ...] `{{dataType}} .

Currently, Show and Eq is supported.

Because this is implemented in Elaborator Reflaction, you must enabele ElabReflection by %language ElabReflection before writing %runElab ....

import Deriving

-- enable ElabReflection
%language ElabReflection

data Janken = Gu | Choki | Pa

-- implement Show and Eq for Janken
%runElab derive [Show, Eq] `{{Janken}}

data StringMaybe = Some String | None

data Result a b = Ok a | Err b

-- implement Show and Eq for StringMaybe
-- and implement Show and Eq for Result a b
%runElab do
  derive [Show, Eq] `{{StringMaybe}}
  derive [Show, Eq] `{{Result}}

Installation

git clone https://github.com/KeenS/idris-deriving.git
cd idris-dervinig
idris --install deriving.ipkg

Then add -p deriving flag when compiling your modules.