Hi, I think everyone has his own proof script styles, and there’s no unique way of indentions fulfilling the favor of everyone. For me, I prefer the following style:
val DIVIDES_0 = store_thm (
"DIVIDES_0”, ``!x. x divides 0``,
metis_tac [divides_def,MULT_CLAUSES]);
or
val DIVIDES_0 = store_thm
("DIVIDES_0",
``!x. x divides 0``,
metis_tac [divides_def,MULT_CLAUSES]);
in which the two appearances of “DIVIDES_0” are perfectly aligned, so that if I
wrongly used different names, I can find out this mistake immediately. The 2nd
argument (the theorem statement) of store_thm, if it’s not short, I will put it
into separated line.
But what’s more important, is to disable the auto-indentation of SML mode, once
I have adjusted my personal-style indentation and hit the RET key to go to next
line. To completely disable SML mode’s auto-indentaion on RET, as suggested in
official HOL emacs manual (originally found by myself), you should put the
following lines into your Emacs configuration: (if you haven’t done this)
(defun my-sml-mode-hook ()
"Local defaults for SML mode"
(setq electric-indent-chars '()))
(add-hook 'sml-mode-hook 'my-sml-mode-hook)
otherwise it will be very very annoying that, your “perfect manually adjusted
indentation” were quickly destroyed once you hit the RET key for going to next
line.
Hope this helps,
Chun Tian
> Il giorno 20 ago 2017, alle ore 00:02, Mario Castelán Castro
> <marioxcc...@yandex.com> ha scritto:
>
> Hello.
>
> Is there some way to make the behavior of auto-indentation in GNU Emacs
> when writing for proof scripts more predictable? By default it uses SML
> mode, which is shipped with Emacs. I can not find any documentation about
> it other than the built-in help, which is not of much use.
>
> I find that SML mode chooses indentation level in an unpredictable way, for
> example, it intend the following code this way:
>
> val DIVIDES_0 =
> store_thm(
> "DIVIDES_0",
> ``!x. x divides 0``,
> metis_tac [divides_def,MULT_CLAUSES]);
>
> (note the extra 2 spaces before “metis_tac”)
>
> If I put “store_thm” in a line of its own, I get an exaggerate amount of
> indentation:
>
> val DIVIDES_0 = store_thm
> ("DIVIDES_0",
> ``!x. x divides 0``,
> metis_tac [divides_def,MULT_CLAUSES]);
>
> Disabling indentation completely (e.g.: M-x fundamental-mode) is not a
> satisfactory solution. Is there some way to make Emacs perform sensible
> indentation for HOL proof scripts?
>
> Thanks in advance.
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org!
> http://sdm.link/slashdot_______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
