introduce a proper view on checkInsert
authorHelmut Grohne <helmut@subdivi.de>
Sat, 12 Jan 2013 16:05:39 +0000 (17:05 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sat, 12 Jan 2013 16:05:39 +0000 (17:05 +0100)
commitf07aa8339d82c98f59f12fc75ea08b2b02bd7354
treed0490deaf71e8283b1dffa037f66645bef508c36
parenta01871259837d6e36c580338f6d29ea0b154ed04
introduce a proper view on checkInsert

Thanks to Joachim Breitner for helping me to work out the definition of
InsertionResult and to Daniel Seidel for helping me understand what
makes a view.
Bidir.agda
CheckInsert.agda