aboutsummaryrefslogtreecommitdiff
path: root/coq/example-utf8.v
diff options
context:
space:
mode:
authorDavid Aspinall2010-08-13 10:26:17 +0000
committerDavid Aspinall2010-08-13 10:26:17 +0000
commita6ea9f91f82c216b9ce756b7323c456eeb80658c (patch)
treec5a3fa6bde88ac23ad42d65aa4c5aa8112e8c319 /coq/example-utf8.v
parent31393e51a20c76084b587e2348d3ba5a8d7c60b2 (diff)
Renamed file
Diffstat (limited to 'coq/example-utf8.v')
-rw-r--r--coq/example-utf8.v26
1 files changed, 0 insertions, 26 deletions
diff --git a/coq/example-utf8.v b/coq/example-utf8.v
deleted file mode 100644
index 4cba17c8..00000000
--- a/coq/example-utf8.v
+++ /dev/null
@@ -1,26 +0,0 @@
-(* -*- coding: utf-8; -*- *)
-
-(* utf8 notations: You can (re)use the version here,
- or a compiled version distributed with Coq IDE:
- Add LoadPath "/usr/lib/coq/ide".
- Require Import utf8.
-*)
-Load "utf8".
-
-(* Printing of unicode notation, in *goals* *)
-Lemma test : ∀ A:Prop, A -> A.
-auto.
-Qed.
-
-(* Parsing of unicode notation here, printing in *goals* *)
-Lemma test2 : ∀ A:Prop, A → A.
-intro.
-intro.
-auto.
-Qed.
-
-(* Printing of unicode notation, in *response* *)
-Check (fun (X:Set)(x:X) => x).
-
-(* Parsing of unicode notation here, printing in *response* *)
-Check (∀A, A→A). \ No newline at end of file