Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Thu, 15 Apr 1993 17:09:25 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA00216;
          Thu, 15 Apr 93 08:55:19 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from bill.cat.syr.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA00211;
          Thu, 15 Apr 93 08:55:09 -0700
Date: Thu, 15 Apr 93 11:55:03 EDT
From: lu@EDU.syr.cat (Juin-Yeu Lu)
Received: by cat.syr.edu (4.1/1.0-6/5/90) id AA00358;
          Thu, 15 Apr 93 11:55:03 EDT
Message-Id: <9304151555.AA00358@cat.syr.edu>
To: shb@com.oracorp
Subject: Simple SML/NJ question
Cc: info-hol@edu.uidaho.cs.ted

Hi Steve,

You asked:

> If
> 
>  val test = [1,2];
>                                                                 
> I'd like to be able to give values to x and y with something like
>
>  val [x,y] = test;

In HOL88, you may use "let" to assign a free variable with a value in a term.

For example,

#set_goal([],"!(A:(num#num)->bool). let (x, y) = (100, 99) in A(y,x)");;
"!A. let (x,y) = (100,99) in A(y,x)"

() : void
#set_goal([],"!(A:(num#num)->bool). let x = 100, 99 in A(SND(x),FST(x))");;
"!A. let x = (100,99) in A(SND x,FST x)"

() : void

   
-Juin-Yeu Lu