Idris: Quadruple

The Idris Quadruple.idr file contains:

To run the Idris program, enter $ idris Quadruple.idr into a Unix-like terminal emulator:

$ idris Quadruple.idr

$ *Quadruple> :t double
double : Int -> Int
$ *Quadruple> double 6
12 : Int
$ *Quadruple> :t quadruple
quadruple : Num a => Int -> Int
$ *Quadruple> quadruple 6
24 : Int

ref. Type-Driven Development with Idris