diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-10-10 16:57:25 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-10-10 16:57:25 +0000 |
| commit | 6fae4cb4715b1a55f6af4a39e1eced4038eace4d (patch) | |
| tree | 1be61881612172da482d64b48985b215c58377cf /coq/coq-unicode-tokens.el | |
| parent | b12a8d0737fbd1179372a8e7774a423c799193c2 (diff) | |
Add some more tokens for making pretty pictures
Diffstat (limited to 'coq/coq-unicode-tokens.el')
| -rw-r--r-- | coq/coq-unicode-tokens.el | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el index 540b6fb5..124a0146 100644 --- a/coq/coq-unicode-tokens.el +++ b/coq/coq-unicode-tokens.el @@ -94,6 +94,19 @@ ("false" "false" bold sans) ("true" "true" bold sans) + ;; example tokens used in Benjamin C. Pierce et al's + ;; Software Foundations course + ("WHILE" "WHILE" bold sans) + ("DO" "DO" bold sans) + ("END" "END" bold sans) + ("SKIP" "SKIP" bold sans) + ("THEN" "THEN" bold sans) + ("ELSE" "ELSE" bold sans) + ("IFB" "IFB" bold sans) + ("FI" "FI" bold sans) + ("{{" "⦃" bold) + ("}}" "⦄" bold) + ;; symbols without utf8.v (but also without context) ("lhd" "⊲") ("rhd" "⊳") @@ -116,9 +129,9 @@ ;; ("==" "≡") ; Setoid equiv (NB: same presentation, pot confusing) - ;; ("-->" "⟹-") ; Morphisms - ;; ("++>" "⟹+") ; - ;; ("==>" "⟹=") ; + ("-->" "⟹-") ; Morphisms + ("++>" "⟹+") ; + ("==>" "⟹") ; (":=" "≔") ("|-" "⊢") |