diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2013-01-14 13:13:00 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2013-01-14 13:13:00 +0100 |
| commit | 9c2be74a5369c1bdb737a67c7c508cb50c62bd83 (patch) | |
| tree | 4b2972936dc6377e2df28b6da3b3485a50296813 /FreeTheorems.agda | |
| parent | a01871259837d6e36c580338f6d29ea0b154ed04 (diff) | |
| download | bidiragda-9c2be74a5369c1bdb737a67c7c508cb50c62bd83.tar.gz | |
define a more useful version of lemma-just\==nnothing
If one had a parameter of type just x \== nothing it could be simply
refuted by case splitting. So the cases where lemma-just\==nnothing was
used always employed trans to combine two results. The new version takes
both results instead.
Diffstat (limited to 'FreeTheorems.agda')
0 files changed, 0 insertions, 0 deletions