Dear Peter,
If you use the Emacs mode to select regions and paste them into a *HOL* buffer
(with M-h M-r), then if you precede that command with two C-u "prefixes", you
get the toggling of quiet-declarations before and after.
So, when I'm opening many theories all at once, I select the relevant
Dear Mike and Anthony,
Thank you so much for your quick responses!
Mike, it turns out I am using Poly/ML, so your solution using
PolyML.print_depth
does work very well for me.
Anthony, I have checked and your solution using HOL_Interactive.toggle_quietdec
also works fine.
Since the toggle_quiet
I use Ramana’s HOL mode for Vim, shortcut “hl”. That makes use of
HOL_Interactive.toggle_quietdec
For example, you can do
> HOL_Interactive.toggle_quietdec();
> open prim_recTheory pairTheory listTheory rich_listTheory;
> open ...
> HOL_Interactive.toggle_quietdec();
The advantage of the Vim
Very often I wish to work in an existing theory script file which begins
with a number of files being opened, e.g.,
open prim_recTheory pairTheory listTheory rich_listTheory;
open combinTheory;
open listLib;
open pred_setTheory pred_setLib;
open numTheory;
open numLib;
open arithmeticTheory;
. . .
Dear All,
Good day!
I want to discharge this goal. Can anyone guide me what property/tactic
can discharge this goal?
0 [`1 <= (i:num) /\ (i:num) <= dimindex (:?122893)`]
1 [`1 <= (i':num) /\ (i':num) <= dimindex (:?122892)`]
`(A:real^N^M)$
(((i:num) - 1) DIV dimindex (:?122884) + 1)$
