Changeset 3575 for LTS/utils.ma


Ignore:
Timestamp:
Jun 19, 2015, 12:00:22 AM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/utils.ma

    r3574 r3575  
    143143qed.
    144144
     145(* some useful deqsets *)
     146
     147definition DeqUnit ≝ mk_DeqSet unit (λ_.λ_.true) ?.
     148@hide_prf ** % // qed.
     149
     150definition DeqFalse ≝ mk_DeqSet False (λ_.λ_.true) ?.
     151@hide_prf * qed.
     152
    145153(* list of elements with decidable equality *)
    146154
Note: See TracChangeset for help on using the changeset viewer.