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
