From c29ccfcf5e194461896eb08d554c80b067b8224a Mon Sep 17 00:00:00 2001 From: "Daniel R. Grayson" Date: Fri, 23 Oct 2015 11:05:54 -0400 Subject: [PATCH] README... --- README.md | 12 ++++++++++++ examples/demo.ctt | 6 ++++++ 2 files changed, 18 insertions(+) diff --git a/README.md b/README.md index ae37811..a9180c7 100644 --- a/README.md +++ b/README.md @@ -64,6 +64,18 @@ To enable the debugging mode add the -d flag. In the interaction loop type :h to get a list of available commands. Note that the current directory will be taken as the search path for the imports. +To enable emacs to edit ```*.ctt``` files in ```ctt-mode```, add the following +line to your ```.emacs``` file: +``` +(autoload 'ctt-mode "cubicaltt" "cubical editing mode" t) +(setq auto-mode-alist (append auto-mode-alist '(("\\.ctt$" . ctt-mode)))) +``` +and ensure that the file ```cubicaltt.el``` is visible in one of the diretories +on emacs' ```load-path```, or else load it in advance, either manually with +```M-x load-file```, or with something like the following line in ```.emacs```: +``` +(load-file "cubicaltt.el") +``` References and notes -------------------- diff --git a/examples/demo.ctt b/examples/demo.ctt index f01b1b8..f2f8e78 100644 --- a/examples/demo.ctt +++ b/examples/demo.ctt @@ -416,3 +416,9 @@ generalize normal inductive types by allowing constructors that define - examples/integer.ctt: The integers as a HIT. -} + +{- +Local Variables: +compile-command: "echo :q | ../cubical demo.ctt" +End: +-} -- 2.34.1