next up previous contents
Next: Natural Numbers: Basic theorems Up: Pure Martin Löf type Previous: Pure Martin Löf type

Basic properties

The module lib_ML contains only one theorem which relates absurd in Prop with empty in SET

 ** Module lib_ML Imports lib_empty lib_unit lib_bool

  absurd_impl_empty = ... : absurd->empty

Fri May 24 19:01:27 BST 1996