I had great difficulty to have HOL prove the following subgoal (I turned on
typing for debugging, ``$c`` is a composition operator like ``$o``):
scf (A :mor -> bool) A (λ(x :mor). x) c sce A (a :mor) = scr A c sce A a
0. homset (A :mor -> bool)
++
The Programming Language Systems Group in the Research School of Computer
Science, The Australian National University has several PhD scholarships and
post-doctoral fellowship opportunities available for bright, enthusiastic
researchers in the following
What did simp[FUNSET_ID, SC_EV] do to this goal, if anything?
I’d expect it to change the goal to
sce A a = scr A c sce A a
(You haven’t shown us any assumptions/theorems about scr.)
Michael
From: Haitao Zhang
Date: Wednesday, 6 March 2019 at 16:57
To: hol-info
Subject: [Hol-info] HOL
I should also add that simp [..] would take a step in the wrong direction
as I have an equality on the assumptions list that I used earlier in the
other direction (through SYM). simp_tac does not do anything as assumptions
are required. And as I can see now the step does not actually depend on
Sorry Michael I cut and pasted the wrong goal for some reason. Here is the
corrected one:
scf (A :mor -> bool) A (λ(x :mor). x) c sce A (a :mor) =
sce A ((λ(x :mor). x) a)
0. homset (A :mor -> bool)
4. (A :mor -> bool) (a :mor)
It doesn't
Hi Michael,
You mentioned an editor mode for SublimeText, can you share a link to it?
Also, I will share this since I didn't notice before: with Vim, you can
"load" files with hl and hL, if they are in directories included in the
Holmakefile INCLUDES variable.
Thank you,
Thomas
On
HOL4 Description Manual provides a detailed description of available
tactics.
http://sourceforge.net/projects/hol/files/hol/kananaskis-12/kananaskis-12-description.pdf/download
-Umair
On Tue, Mar 5, 2019 at 11:09 AM Gergely Buday wrote:
> Hi,
>
> I'm learning HOL tactics and started to
Question:
Who did derive the division by zero 1/0 and the division by zero calculus
$\tan(\pi/2)=0, \log 0=0$ as the outputs of a computer?
Facts:
On February 16, 2019 Professor H. Okumura introduced the surprising news in
Research Gate:
José Manuel Rodríguez Caballero\\
Added an answer\\
It’s available at https://github.com/HOL-Theorem-Prover/SublimeHOL
I believe you can install packages directly into Sublime Text by providing such
URLs.
Michael
From: Thomas Lacroix
Date: Tuesday, 5 March 2019 at 19:17
To: "Norrish, Michael (Data61, Acton)"
Cc: hol-info
Subject: Re:
