Exploring Idris: Reflexivity Tactics one up Unit Tests

Idris the Dragon, inspiration for the language
namespace Booleans     data Bool = True | False     not : Booleans.Bool -> Booleans.Bool
not True = False
not False = True
proofNotTrue : (not True) = False
proofNotTrue = Refl
proofNotFalse : (not False) = True
proofNotFalse = Refl

--

--

--

A 25 year software industry veteran with a passion for functional programming, architecture, mentoring / team development, xp/agile and doing the right thing.

Love podcasts or audiobooks? Learn on the go with our new app.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Todd Brown

Todd Brown

A 25 year software industry veteran with a passion for functional programming, architecture, mentoring / team development, xp/agile and doing the right thing.

More from Medium

Scisprint February in Hsinchu

Demystifying Web Workers

Working of web worker

Paheli — पहेली – a riddle, wordle

Interview with Maurizio Conza