Dear all,
I am working in HOL Light and I want to verify the following theorem
regarding integrability of a vector function:
*f integrable_on (:real^1) ==> f integrable_on {t | a <= drop t}*
which says that if a function is integrable on (-inf, inf) then it is
integrable on its subset which look
It's a bit confusing. The expressions you enter in the session are not
actually in HOL - they are in the functional programming language ML.
This is the language used to implement HOL4. You are in an ML toplevel
(also called "read-eval-print loop" or "REPL"), with HOL4 already
incorporated. ML
FST is a function in logic, not in ML.
In this case, there does happen to be a similar function, called fst, in ML.
Are you trying to specify/prove something in logic? Or are you trying to
write an ML program?
On 22 June 2016 at 18:21, Ada <956066...@qq.com> wrote:
> Hi,guys
> I am work
Hi,guys
I am working with HOL4.
FST is in pairTheory, its definition is
[FST] Theorem |- ∀x y. FST (x,y) = x But, When I use it like
following: val n = FST (1,2); It responses:! Toplevel input:
! val n = FST (1,2);
! ^^^
! Type clash
