-
Notifications
You must be signed in to change notification settings - Fork 0
/
LibUnit.v
51 lines (35 loc) · 1.58 KB
/
LibUnit.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
(* This file is extracted from the TLC library.
http://github.com/charguer/tlc
DO NOT EDIT. *)
(**************************************************************************
* Product of Data Structures *
**************************************************************************)
Set Implicit Arguments.
From SLF Require Import LibTactics LibLogic LibReflect.
(* ********************************************************************** *)
(* ################################################################# *)
(** * Unit type *)
(* ---------------------------------------------------------------------- *)
(* ================================================================= *)
(** ** Definition *)
(** From the Prelude.
Inductive unit : Type :=
| tt : unit.
Add Printing If bool.
Delimit Scope bool_scope with bool.
*)
(* ---------------------------------------------------------------------- *)
(* ================================================================= *)
(** ** Inhabited *)
Instance Inhab_unit : Inhab unit.
Proof using. intros. apply (Inhab_of_val tt). Qed.
(* ********************************************************************** *)
(* ################################################################# *)
(** * Properties *)
(* ---------------------------------------------------------------------- *)
(* ================================================================= *)
(** ** Uniqueness *)
Lemma unit_eq : forall (tt1 tt2 : unit),
tt1 = tt2.
Proof using. intros. destruct tt1. destruct~ tt2. Qed.
(* 2021-01-25 13:22 *)