generalize checkInsert to arbitrary Setoids
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 17 Jan 2014 08:24:47 +0000 (09:24 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 17 Jan 2014 08:24:47 +0000 (09:24 +0100)
commit808b8da4b14b087c0dcace71fff3854a17cebe42
tree213872ff0a7165dee7a9510f75d78d7b76ccc015
parent5bf7ce31ca6928b13d6631591371e98933cb0b2d
generalize checkInsert to arbitrary Setoids

This is another step towards permitting arbitrary Setoids in bff.
BFF.agda
Bidir.agda
CheckInsert.agda
Precond.agda