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
