source: Deliverables/D4.1/DemoFinal/matita/Compare.ma

Last change on this file was 671, checked in by mulligan, 10 years ago

Finished demo script for tomorrow.
File size: 110 bytes
Line 
1include "logic/pts.ma".
2
3ninductive Compare: Type[0] ≝
4  Equal: Compare
5| Less: Compare
6| Greater: Compare.
Note: See TracBrowser for help on using the repository browser.