IT/Description/system.tex

14 con l'\ML. Se non lo �, dovrebbe leggere prima l'introduzione all'\ML\ in {\sl Getting Started
47 di nomi che sono identificatori (si veda la Sezione~\ref{ident} di sotto). Usare dei non-identificatori come nomi di variabili � sconsigliato eccetto in circostanze
55 alfanumerico che a sua volta non contiene apici (si veda la Sezione~\ref{tyvars}
98 	sono chiamati caratteri \emph{non-aggreganti}. %
100   \index{identificatori, nella logica HOL@identificatori, nella logica \HOL{}!caratteri non-aggreganti}%
102   A meno che il token desiderato non sia gi� presente nella grammatica, questi
103 	caratteri non si combinano tra di loro o con altri caratteri
109   I caratteri unicode che non sono n� lettere n� cifre sono considerati
110 	come simboli. Nessuno di questi � non-aggregante.
112 \item Un \emph{numero} � una stringa di una o pi� cifre. Se non � la
139 dei booleani, e di conseguenza anche in tutte le teorie discendenti. Essi non
151 non contiene primi; per esempio tutti quelli che seguono sono nomi validi
164 ha token speciali (l'``if'', il ``then'' e l'``else'') che non sono nomi per le variabili, n� per le costanti (la costante sottostante � di fatto chiamata \holtxt{COND}).
165 Per essere sicuro che le operazioni di stampa e parsing dei token siano appropriatamente l'una l'inverso dell'altra, gli utenti non dovrebbero creare token che includono spazi vuoti o le stringhe di commento (\ml{(*} and \ml{*)}).
197 con un nome dato; essa da un warning se il nome non � un nome ammissibile
198 per una variabile di tipo (cio� non � un \ml{'} seguito da un alfanumerico).
209 (in \LOGIC, tuttavia, i tipi funzioni non erano considerati come tipi
219 \item $\mathit{name}$ non � un tipo operatore della teoria $\mathit{thyname}$
221 ma la sua ariet� non � $n$.
233 legate a valori \ML\ e non hanno bisogno di essere costruiti ripetutamente, ad esempio il tipo costruito da\linebreak
321 \item $c$ non � il nome di una costante nella teoria $\mathit{thyname}$;
322 \item $\sigma$ non � un'istanza del tipo generico di $c$
343 \item il tipo di $t_1$ non ha la forma \ml{$\sigma'$->$\sigma$};
345 tipo di $t_2$ non � uguale a $\sigma'$.
360 $\lquant{x}t$; essa fallisce se $x$ non � una variabile.
514 Si noti che non c'� alcuna informazione esplicita di tipo in
518 \holtxt{\bs{}x.x+1} potrebbero avere il tipo \holtxt{num}. Questa non �
650     (80)   TM  ::=  TM ":-" TM   (non-associative)
651     (100)  TM  ::=  TM "=" TM   (non-associative)
655     (425)  TM  ::=  TM "IN" TM   (non-associative)
691 l'overload, non solo i numerali. A volte una tale flessibilit� � piuttosto
706 Si noti come il simbolo \holtxt{<} non sia trattato come un infisso dal
708 token non � mai dato un trattamento speciale dal parser della sintassi
866   una lista, non un insieme; cio�, sono ordinati.}. Fu quindi definito il concetto di un sequente
968 di un teorema. Il tipo \ML\ non ha
971 dalla costruzione arbitraria e non tracciata
1082 bench� \ml{thm} non abbia dei costruttori primitivi, esso ha (otto)
1119 Fallisce se $t$ non � di tipo \ml{bool}.
1139 {\small\verb+|- +}$t${\small\verb+ = +}$t$. Una chiamata a \ml{REFL} non fallisce mai.
1170 Fallisce se l'argomento a \ml{BETA\_CONV} non � un $\beta$-redex
1171 (cio� non � della forma \holtxt{(\bs$x$.$t_1$)$t_2$}.
1224 \item il tipo di $x_i$ non � uguale al tipo di $t_i$ per qualche
1246 \item dove $x$ non � libera in $\Gamma$.
1252 Fallisce se $x$ non � una variabile, o $x$
1291 $\sigma_i$ (per $1 \leq i \leq n$). Si verifica un fallimento se un $\alpha_i$ non
1319 da $\Gamma$ (si noti che non � necessario che $t_1$ occorra in $\Gamma$; in questo caso
1327 \ml{DISCH} fallisce se il termine dato come suo primo argomento non � di
1352 il risultato dell'applicazione del Modus Ponens; fallisce se gli argomenti non sono della
1365 Per evitare la non validit�, � attaccato un \emph{tag} a ogni teorema che deriva
1468 teoria non � realmente un concetto logico, ma piuttosto un mezzo per
1583 di una chiamata a {\small\verb+new_theory +}$thy_2$ non � vuota, cio�, � stato
1593 \item $name$ non � un alfanumerico che inizia con una lettera.
1610 o cancellato sarebbe quindi considerato {\it scaduto}, e non sarebbe
1615 Contrariamente al segmento attuale, i segmenti antenati (propri) non possono
1637 continui. Si noti che {\small\verb+load+} non pu� essere usato in file ML
1638 che non sono stati compilati; pu� essere usato solo nel sistema
1644 attuale. Nell'uso tipico, queste funzioni non saranno
1660 \ty{op} non � un nome permesso per un tipo, sar� emesso un warning.
1676 Se $c$ non � un nome permesso per una costante, sar� emesso un warning.
1690 \item il tipo di $t$ non � \verb+bool+.
1733 la teoria esportata non � compilata da \HOL. Questo � lasciato a uno
1754 non possono essere estese in questo modo; esse possono essere pensate come
1839 \item $c$ non � il nome di alcuna costante in $\Sigma_{\Omega}$;
1878 \item $t$ contiene delle variabili libere che non sono in nessuna delle
1882 che non occorre nel tipo di $c$.
1942 \item il teorema argomento non ha una lista vuota di assunzioni;
1944 \item $c_1$, $\dots$, $c_n$ non sono variabili distinte;
1945 \item il tipo di qualche $c_i$ non contiene tutte le variabili
1972 sottoinsieme non vuoto di un tipo esistente $\sigma$. Formalmente, una definizione di tipo
2034 \item $t$ non ha un tipo della forma $\sigma$\ml{->bool}.
2102 \item $th$ non � un teorema della forma restituita da
2169 \noindent Tutte e quattro le funzioni falliranno se applicate a qualunque teorema che non