Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: shaw@cs.ucdavis.edu (Rob Shaw)
Date: Fri, 26 Jan 1996 16:30:18 -0800
Message-Id: <199601270030.QAA01217@roma-cafe.cs.ucdavis.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Blank Pattern in HOL90 ?
Content-Length: 714


I am embedding some SML code into HOL90 to reason about it, and have 
noticed that the blank pattern has changed from HOL88:

#"let (_,x,_) = (1,2,3) in x";;
"let (_,x,_) = (1,2,3) in x" : term
 

In HOL90:

--`let ( _ ,x) = (1,2) in x`--;
HOL parser error: syntax error

Exception raised at Parse.first pass of parsing:
syntax error

uncaught exception HOL_ERR


This would lead me to think that the blank pattern is gone. However,
it looks as though blank is at least a legal identiter sometimes:

- --`_ :num`--;
val it = (--`_`--) : term
- 

Questions:

What kind of ident is blank, that it is not allowed in a let VSTRUCT 
binding but can serve as variable?

Is there any blank pattern now?

Thanx, 

Rob