diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2017-03-02 11:07:56 -0500 |
|---|---|---|
| committer | Paul Steckler <steck@stecksoft.com> | 2017-03-02 11:07:56 -0500 |
| commit | a1278112e8a613069bbfb9fa47bee2b9089efd4a (patch) | |
| tree | 5b174d02839c16a8cf00b800efc13fc16544d116 /coq/ex | |
| parent | a424cf37d41c7d9c7443132a385b89f3947bc708 (diff) | |
use Utf8 from Coq library
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/example-utf8.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/coq/ex/example-utf8.v b/coq/ex/example-utf8.v index 4cba17c8..0f528f14 100644 --- a/coq/ex/example-utf8.v +++ b/coq/ex/example-utf8.v @@ -1,11 +1,6 @@ (* -*- 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". +Require Import Utf8. (* Printing of unicode notation, in *goals* *) Lemma test : ∀ A:Prop, A -> A. @@ -23,4 +18,4 @@ Qed. 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 +Check (∀A, A→A). |