Lib (nholz)

Lib Module

Namespace: HOL
Assembly: nholz.dll

Questo modulo definisce varie utilità di programmazione funzionale da usare nel corso dell'implementazione.

Functions and values

Function or value	Description
`(<) f g x` Full Usage: `(<) f g x` Parameters: f : `'c -> 'd` g : `'e -> 'c` x : `'e` Returns: `'d`	La funzione binaria infissa per la composizione di funzioni. Corrisponde a <<. f : `'c -> 'd` g : `'e -> 'c` x : `'e` Returns: `'d`
`(\|\|>>) f g (x, y)` Full Usage: `(\|\|>>) f g (x, y)` Parameters: f : `'a -> 'b` g : `'c -> 'd` x : `'a` y : `'c` Returns: `'b * 'd`	f : `'a -> 'b` g : `'c -> 'd` x : `'a` y : `'c` Returns: `'b * 'd`
`append xs ys` Full Usage: `append xs ys` Parameters: xs : `'a list` ys : `'a list` Returns: `'a list`	Concatena insieme le due liste fornite. Si tratta della forma non infissa e curried di '@' xs : `'a list` ys : `'a list` Returns: `'a list`
`arg1_fn x y` Full Usage: `arg1_fn x y` Parameters: x : `'a` y : `'b` Returns: `'a`	La funzione binaria curried che restituisce il suo primo argomento. E' chiamata il combinatore 'K' nella logica combinatoria. x : `'a` y : `'b` Returns: `'a`
`assert0 b e` Full Usage: `assert0 b e` Parameters: b : `bool` e : `Exception`	Solleva l'eccezione fornita se il boleano fornito è "false", altrimenti restituisce unit. b : `bool` e : `Exception`
`assert1 b (func, msg)` Full Usage: `assert1 b (func, msg)` Parameters: b : `bool` func : `string` msg : `string`	Solleva un'eccezione HolFail per il nome di funzione e il messaggio forniti se il boleano fornito è "false", e altrimenti restituisce unit. b : `bool` func : `string` msg : `string`
`assoc x xys` Full Usage: `assoc x xys` Parameters: x : `'a` xys : `('a * 'b) list` Returns: `'b`	Restituisce il componente destro della prima coppia nella lista fornita il cui componente sinistro è uguale al valore fornito. Fallisce se non può trovare una tale coppia. x : `'a` xys : `('a * 'b) list` Returns: `'b`
`can f x` Full Usage: `can f x` Parameters: f : `'a -> 'b` x : `'a` Returns: `bool`	Restituisce "true" sse applicare la funzione fornita all'argomento fornito non causa un'eccezione HolFail. f : `'a -> 'b` x : `'a` Returns: `bool`
`cannot f x` Full Usage: `cannot f x` Parameters: f : `'a -> 'b` x : `'a` Returns: `bool`	Restituisce "true" sse applicare la funzione fornita all'argomento fornito causa un'eccezione HolFail. f : `'a -> 'b` x : `'a` Returns: `bool`
`char_escape c` Full Usage: `char_escape c` Parameters: c : `char` Returns: `string`	c : `char` Returns: `string`
`char_explode x` Full Usage: `char_explode x` Parameters: x : `string` Returns: `char list`	Divide una stringa in una lista di caratteri. x : `string` Returns: `char list`
`char_implode cs` Full Usage: `char_implode cs` Parameters: cs : `char list` Returns: `string`	Concatena una lista di caratteri in una singola stringa. cs : `char list` Returns: `string`
`check p x` Full Usage: `check p x` Parameters: p : `'a -> bool` x : `'a` Returns: `'a`	Solleva un'eccezione HolFail se l'argomento fornito non soddisfa la funzione di test passata, altrimenti restituisce l'argomento. p : `'a -> bool` x : `'a` Returns: `'a`
`cons x xs` Full Usage: `cons x xs` Parameters: x : `'a` xs : `'a list` Returns: `'a list`	Aggiunge un dato elemento all'inizio di una lista data. Si tratta di una forma non infissa e curried di '::'. x : `'a` xs : `'a list` Returns: `'a list`
`curry f x y` Full Usage: `curry f x y` Parameters: f : `'a * 'b -> 'c` x : `'a` y : `'b` Returns: `'c`	Restituisce l'equivalente curried di una funzione binaria che prende una coppia come argomento. f : `'a * 'b -> 'c` x : `'a` y : `'b` Returns: `'c`
`cut n xs` Full Usage: `cut n xs` Parameters: n : `int` xs : `'a list` Returns: `'a list * 'a list`	Divide la lista fornita in due secondo l'indice 'n' a base 1, con gli elementi da 1 a 'n' nella prima lista e i restanti nella seconda. Fallisce se 'n' è negativo o maggiore della lnghezza della lista. n : `int` xs : `'a list` Returns: `'a list * 'a list`
`cut_while p xs` Full Usage: `cut_while p xs` Parameters: p : `'d -> bool` xs : `'d list` Returns: `'d list * 'd list`	Divide la lista fornita in due segmenti, dove il secondo segmento inizia al primo elemento che non soddisfa la funzione di test fornita. p : `'d -> bool` xs : `'d list` Returns: `'d list * 'd list`
`cut_while0 p ys xs` Full Usage: `cut_while0 p ys xs` Parameters: p : `'a -> bool` ys : `'a list` xs : `'a list` Returns: `'a list * 'a list`	Funzione tail-ricorsiva a supporto della definizione di cut_while p : `'a -> bool` ys : `'a list` xs : `'a list` Returns: `'a list * 'a list`
`dbl_arg f x` Full Usage: `dbl_arg f x` Parameters: f : `'a -> 'a -> 'b` x : `'a` Returns: `'b`	Applica la funzione binaria curried fornita usando l'argomento fornito per entrambi gli argomenti della funzione. E' chiamata il combinatore 'W' nella logica combinatoria. f : `'a -> 'a -> 'b` x : `'a` Returns: `'b`
`decrement n` Full Usage: `decrement n` Parameters: n : `int` Returns: `int`	Sottrae 1 se l'intero fornito è positivo, altrimenti restituisce 0. n : `int` Returns: `int`
`disjoint xs ys` Full Usage: `disjoint xs ys` Parameters: xs : `'a list` ys : `'a list` Returns: `bool`	Restituisce "true" sse non ci sono elementi in comune tra le due liste fornite. xs : `'a list` ys : `'a list` Returns: `bool`
`disjoint' eq xs ys` Full Usage: `disjoint' eq xs ys` Parameters: eq : `'a -> 'b -> bool` xs : `'a list` ys : `'b list` Returns: `bool`	Restituisce "true" sse non ci sono elementi in comune tra le due liste fornite rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'b -> bool` xs : `'a list` ys : `'b list` Returns: `bool`
`do_map f xs` Full Usage: `do_map f xs` Parameters: f : `'a -> unit` xs : `'a list`	Applica la funzione con valore unit fornita a turno su ciascun elemento della lista fornita, restituendo a sua volta unit. f : `'a -> unit` xs : `'a list`
`el n xs` Full Usage: `el n xs` Parameters: n : `int` xs : `'f list` Returns: `'f`	Restituisce l'n-esimo elemento della lista fornita, usando una base 1 d'indicizzazione. Fallisce se l'indice è fuori dal range. n : `int` xs : `'f list` Returns: `'f`
`el0 n xs` Full Usage: `el0 n xs` Parameters: n : `int` xs : `'a list` Returns: `'a`	Restituisce l'n-esimo elemento della lista fornita, usando una base 0 d'indicizzazione. Fallisce se l'indice è fuori dal range. n : `int` xs : `'a list` Returns: `'a`
`enumerate xs` Full Usage: `enumerate xs` Parameters: xs : `'a list` Returns: `(int * 'a) list`	Etichetta ciascun elemento della lista fornita con la sua posizione (a base 1) nella lista. xs : `'a list` Returns: `(int * 'a) list`
`enumerate0 n xs` Full Usage: `enumerate0 n xs` Parameters: n : `int` xs : `'a list` Returns: `(int * 'a) list`	Funzione tail-ricorsiva a supporto della definizione di enumerate n : `int` xs : `'a list` Returns: `(int * 'a) list`
`exists p xs` Full Usage: `exists p xs` Parameters: p : `'a -> bool` xs : `'a list` Returns: `bool`	Restituisce "true" sse c'è almento un elemento nella lista fornita che soddisfa una data funzione di test. p : `'a -> bool` xs : `'a list` Returns: `bool`
`explode x` Full Usage: `explode x` Parameters: x : `string` Returns: `string list`	Divide una stringa in una lista di stringhe da un solo carattere. x : `string` Returns: `string list`
`filter p xs` Full Usage: `filter p xs` Parameters: p : `'b -> bool` xs : `'b list` Returns: `'b list`	Rimuove tutti gli elementi della lista fornita che non soddisfano una data funzione di test. p : `'b -> bool` xs : `'b list` Returns: `'b list`
`find p xs` Full Usage: `find p xs` Parameters: p : `'a -> bool` xs : `'a list` Returns: `'a`	Restituisce il primo elemento della lista fornita che soddisfa una data funzione di test. Fallisce se un tale elemento non esiste. p : `'a -> bool` xs : `'a list` Returns: `'a`
`flatten xss` Full Usage: `flatten xss` Parameters: xss : `'a list list` Returns: `'a list`	Appiattisce la lista di liste fornita in una lista singola. xss : `'a list list` Returns: `'a list`
`foldl f a xs` Full Usage: `foldl f a xs` Parameters: f : `'a -> 'b -> 'a` a : `'a` xs : `'b list` Returns: `'a`	Applica l'operatore binario curried fornito sugli elementi della lista fornita, da sinistra a destra, iniziando con l'operatore applicato all'argomento extra fornito e al primo elemento della lista. Restituisce l'argomento extra se la lista è vuota. foldl (+) a [x1;x2;..;xn] == (..((a + x1) + x2) + ..) + xn f : `'a -> 'b -> 'a` a : `'a` xs : `'b list` Returns: `'a`
`foldl' mk_fn (x, xs)` Full Usage: `foldl' mk_fn (x, xs)` Parameters: mk_fn : `'a * 'b -> 'a` x : `'a` xs : `'b list` Returns: `'a`	Versione uncurried di foldl mk_fn : `'a * 'b -> 'a` x : `'a` xs : `'b list` Returns: `'a`
`foldl1 f xs` Full Usage: `foldl1 f xs` Parameters: f : `'a -> 'a -> 'a` xs : `'a list` Returns: `'a`	Applica l'operatore binario curried fornito sugli elementi della lista fornita, da sinistra a destra. Fallisce se la lista è vuota. foldl1 (+) [x1;x2;..;xn] == (..(x1 + x2) + ..) + xn f : `'a -> 'a -> 'a` xs : `'a list` Returns: `'a`
`foldl1' mk_fn xs` Full Usage: `foldl1' mk_fn xs` Parameters: mk_fn : `'a * 'a -> 'a` xs : `'a list` Returns: `'a`	Versione uncurried di foldl1 mk_fn : `'a * 'a -> 'a` xs : `'a list` Returns: `'a`
`foldr f xs a` Full Usage: `foldr f xs a` Parameters: f : `'a -> 'b -> 'b` xs : `'a list` a : `'b` Returns: `'b`	Applica l'operatore binario curried fornito sugli elementi della lista fornita, da destra a sinistra, iniziando con l'operatore applicato all'ultimo elemento della lista e all'argomento extra fornito. Restituisce l'argomento estra se la lista è vuota. foldr (+) [x1;x2;..;xn] a == x1 + (x2 + (.. + (xn + a)..)) f : `'a -> 'b -> 'b` xs : `'a list` a : `'b` Returns: `'b`
`foldr' mk_fn (xs, x)` Full Usage: `foldr' mk_fn (xs, x)` Parameters: mk_fn : `'a * 'b -> 'b` xs : `'a list` x : `'b` Returns: `'b`	Versione uncurried di foldr mk_fn : `'a * 'b -> 'b` xs : `'a list` x : `'b` Returns: `'b`
`foldr1 f xs` Full Usage: `foldr1 f xs` Parameters: f : `'a -> 'a -> 'a` xs : `'a list` Returns: `'a`	Applica un dato operatore binario curried sugli elementi della lista fornita, da destra a sinistra. Fallisce se la lista è vuota. foldr1 (+) [x1;x2;..;xn] == x1 + (x2 + .. + (xn-1 + xn)..) f : `'a -> 'a -> 'a` xs : `'a list` Returns: `'a`
`foldr1' mk_fn xs` Full Usage: `foldr1' mk_fn xs` Parameters: mk_fn : `'a * 'a -> 'a` xs : `'a list` Returns: `'a`	Versione uncurried di foldr1' mk_fn : `'a * 'a -> 'a` xs : `'a list` Returns: `'a`
`forall p xs` Full Usage: `forall p xs` Parameters: p : `'a -> bool` xs : `'a list` Returns: `bool`	Restituisce "true" sse ogni elemento nella lista fornita soddisfa una data funzione di test. p : `'a -> bool` xs : `'a list` Returns: `bool`
`forall2 p l1 l2` Full Usage: `forall2 p l1 l2` Parameters: p : `'a -> 'b -> bool` l1 : `'a list` l2 : `'b list` Returns: `bool`	Testa se gli elementi corrispondenti di due liste soddisfano tutte una relazionze. p : `'a -> 'b -> bool` l1 : `'a list` l2 : `'b list` Returns: `bool`
`front xs` Full Usage: `front xs` Parameters: xs : `'a list` Returns: `'a list`	Funzione per estrarre da una lista tutti gli elementi escluso l'ultimo. Fallisce se la lista è vuota. xs : `'a list` Returns: `'a list`
`front_last xs` Full Usage: `front_last xs` Parameters: xs : `'a list` Returns: `'a list * 'a`	Funzione per dividere una lista fornita nei suoi primi elementi e nel suo ultimo. Fallisce se la lista è vuota. xs : `'a list` Returns: `'a list * 'a`
`fst_filter p xys` Full Usage: `fst_filter p xys` Parameters: p : `'a -> bool` xys : `('a * 'b) list` Returns: `('a * 'b) list`	Elimina dalla lista di coppie fornita gli elementi con un componente sinistro che restituisce falso per la funzione di test fornita. p : `'a -> bool` xys : `('a * 'b) list` Returns: `('a * 'b) list`
`fst_map f xys` Full Usage: `fst_map f xys` Parameters: f : `'a -> 'b` xys : `('a * 'c) list` Returns: `('b * 'c) list`	Applica la funzione fornita al componente sinistro di ciascuna coppia nella lista di coppie fornita. f : `'a -> 'b` xys : `('a * 'c) list` Returns: `('b * 'c) list`
`funpow n f x` Full Usage: `funpow n f x` Parameters: n : `int` f : `'a -> 'a` x : `'a` Returns: `'a`	Applica l'ennesima potenza della funzione fornita. cioè esegue una ricorsione della funzione n volte, passando il risultato nuovamente come input, e restituendo l'input originario se n è 0. Fallisce se la potenza è negativa. n : `int` f : `'a -> 'a` x : `'a` Returns: `'a`
`hd xs` Full Usage: `hd xs` Parameters: xs : `'a list` Returns: `'a`	Funzione per estrarre da una lista fornita il suo elemento di testa. Fallisce se la lista è vuota. xs : `'a list` Returns: `'a`
`hd_tl xs` Full Usage: `hd_tl xs` Parameters: xs : `'a list` Returns: `'a * 'a list`	Funzione per dividere una lista fornita nella sua testa e nella sua coda. Fallisce se la lista è vuota. xs : `'a list` Returns: `'a * 'a list`
`id_fn x` Full Usage: `id_fn x` Parameters: x : `'a` Returns: `'a`	La funzione che restituisce il suo argomento come suo risultato. E' chiamata il combinatore 'I' nella logica combinatoria. x : `'a` Returns: `'a`
`implode xs` Full Usage: `implode xs` Parameters: xs : `string list` Returns: `string`	Concatena una lista di stringhe in una singola stringa. xs : `string list` Returns: `string`
`insert x xs` Full Usage: `insert x xs` Parameters: x : `'a` xs : `'a list` Returns: `'a list`	Aggiunge l'elemento fornito alla lista fornita a meno che sia già nella lista. x : `'a` xs : `'a list` Returns: `'a list`
`insert' eq x xs` Full Usage: `insert' eq x xs` Parameters: eq : `'a -> 'a -> bool` x : `'a` xs : `'a list` Returns: `'a list`	Aggiunge l'elemento fornto alla lista fornita a meno che sia già nella lista rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'a -> bool` x : `'a` xs : `'a list` Returns: `'a list`
`int_of_string str` Full Usage: `int_of_string str` Parameters: str : `string` Returns: `int`	str : `string` Returns: `int`
`intersect xs1 xs2` Full Usage: `intersect xs1 xs2` Parameters: xs1 : `'a list` xs2 : `'a list` Returns: `'a list`	Crea una lista di elementi che occorrono in ciasuna delle due liste fornite. xs1 : `'a list` xs2 : `'a list` Returns: `'a list`
`intersect' eq xs1 xs2` Full Usage: `intersect' eq xs1 xs2` Parameters: eq : `'a -> 'b -> bool` xs1 : `'a list` xs2 : `'b list` Returns: `'a list`	Crea una lista di elementi che occorrono in ciasuna delle due liste fornite rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'b -> bool` xs1 : `'a list` xs2 : `'b list` Returns: `'a list`
`inv_assoc y xys` Full Usage: `inv_assoc y xys` Parameters: y : `'a` xys : `('b * 'a) list` Returns: `'b`	Restituisce il componente sinistro della prima coppia nella lista fornita il cui componente destro è uguale al valore fornito. Fallisce se non può trovare una tale coppia. y : `'a` xys : `('b * 'a) list` Returns: `'b`
`is_empty xs` Full Usage: `is_empty xs` Parameters: xs : `'b list` Returns: `bool`	Restituisce "true" sse la lista fornita è vuota. xs : `'b list` Returns: `bool`
`is_nonempty xs` Full Usage: `is_nonempty xs` Parameters: xs : `'b list` Returns: `bool`	Restituisce "true" sse la lista fornita non è vuota. xs : `'b list` Returns: `bool`
`last xs` Full Usage: `last xs` Parameters: xs : `'a list` Returns: `'a`	Funzione per estrarre l'ultimo elemento di una lista fornita. Fallisce se la lista è vuota. xs : `'a list` Returns: `'a`
`length xs` Full Usage: `length xs` Parameters: xs : `'a list` Returns: `int`	Restituisce la lunghezza della lista fornita. xs : `'a list` Returns: `int`
`length0 n xs` Full Usage: `length0 n xs` Parameters: n : `int` xs : `'a list` Returns: `int`	Funzione tail recursive di supporto alla definizione di length. n : `int` xs : `'a list` Returns: `int`
`length_big_int` Full Usage: `length_big_int` Returns: `'a list -> BigInteger`	Restituisce la lunghezza della lista fornita come un intero f# di precisione arbitraria. Returns: `'a list -> BigInteger`
`list_eq eq xs ys` Full Usage: `list_eq eq xs ys` Parameters: eq : `'a -> 'b -> bool` xs : `'a list` ys : `'b list` Returns: `bool`	Resituisce "true" sse le due liste di input sono equivalenti modulo la relazione di equivalenza fornita 'eq', cioè se le liste hanno la stessa lunghezza e gli elementi corrispondenti sono uguali secondo 'eq'. eq : `'a -> 'b -> bool` xs : `'a list` ys : `'b list` Returns: `bool`
`map f xs` Full Usage: `map f xs` Parameters: f : `'a -> 'b` xs : `'a list` Returns: `'b list`	Applicala funzione fornita a ciascun elemento della lista fornita. map f [x1;x2;..;xn] == [f x1; f x2; ..; f xn] f : `'a -> 'b` xs : `'a list` Returns: `'b list`
`map2 f xs ys` Full Usage: `map2 f xs ys` Parameters: f : `'a -> 'b -> 'c` xs : `'a list` ys : `'b list` Returns: `'c list`	Applica una data funzione binaria curried agli elementi corrispondenti di due liste date. Fallisce se le liste non hanno la stessa lunghezza. map2 (+) [x1;x2;..;xn] [y1;y2;..;yn] = [x1 + y1; x2 + y2; ..; xn + yn] f : `'a -> 'b -> 'c` xs : `'a list` ys : `'b list` Returns: `'c list`
`mem x xs` Full Usage: `mem x xs` Parameters: x : `'b` xs : `'b list` Returns: `bool`	Restituisce "true" sse l'elemento fornito è nella lista fornita. x : `'b` xs : `'b list` Returns: `bool`
`mem' eq x xs` Full Usage: `mem' eq x xs` Parameters: eq : `'a -> 'b -> bool` x : `'a` xs : `'b list` Returns: `bool`	Restituisce "true" sse l'elemento fornito è nella lista fornita rispetto a una funzione di confronto passata come argomento. eq : `'a -> 'b -> bool` x : `'a` xs : `'b list` Returns: `bool`
`merge r xs ys` Full Usage: `merge r xs ys` Parameters: r : `'a -> 'a -> bool` xs : `'a list` ys : `'a list` Returns: `'a list`	Fa il merge delle due liste ordinate fornite in un'unica lista ordinata, rispetto alla relazione di ordinamento totale fornita. r : `'a -> 'a -> bool` xs : `'a list` ys : `'a list` Returns: `'a list`
`mergesort r xs` Full Usage: `mergesort r xs` Parameters: r : `'a -> 'a -> bool` xs : `'a list` Returns: `'a list`	Ordina la lista fornita usando la tecnica del merge, rispetto alla relazione di orinamento totale fornita. r : `'a -> 'a -> bool` xs : `'a list` Returns: `'a list`
`no_dups xs` Full Usage: `no_dups xs` Parameters: xs : `'a list` Returns: `bool`	Restituisce "true" sse la lista fornita non contiene duplicati. xs : `'a list` Returns: `bool`
`no_dups' eq xs` Full Usage: `no_dups' eq xs` Parameters: eq : `'a -> 'a -> bool` xs : `'a list` Returns: `bool`	Restituisce "true" sse la lista fornita non contiene duplicati rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'a -> bool` xs : `'a list` Returns: `bool`
`no_dups0 xs0 xs` Full Usage: `no_dups0 xs0 xs` Parameters: xs0 : `'a list` xs : `'a list` Returns: `bool`	Funzione tail ricorsiva a supporto della definizione di no_dups xs0 : `'a list` xs : `'a list` Returns: `bool`
`no_dups0' eq xs0 xs` Full Usage: `no_dups0' eq xs0 xs` Parameters: eq : `'a -> 'a -> bool` xs0 : `'a list` xs : `'a list` Returns: `bool`	Funzione tail ricorsiva a supporto della definizione di no_dups' eq : `'a -> 'a -> bool` xs0 : `'a list` xs : `'a list` Returns: `bool`
`pair x y` Full Usage: `pair x y` Parameters: x : `'a` y : `'b` Returns: `'a * 'b`	L'operatore binario curried per costruire coppie. x : `'a` y : `'b` Returns: `'a * 'b`
`pair_apply (f, g) (x, y)` Full Usage: `pair_apply (f, g) (x, y)` Parameters: f : `'a -> 'b` g : `'c -> 'd` x : `'a` y : `'c` Returns: `'b * 'd`	Applica la coppia di funzioni fornita ai componenti corrispondenti di una coppia data f : `'a -> 'b` g : `'c -> 'd` x : `'a` y : `'c` Returns: `'b * 'd`
`partition p xs` Full Usage: `partition p xs` Parameters: p : `'a -> bool` xs : `'a list` Returns: `'a list * 'a list`	Separa la lista fornita in due lista, per quegli elementi che rispettivamente soddisfano e non soddisfano una data funzione di test. p : `'a -> bool` xs : `'a list` Returns: `'a list * 'a list`
`quote x` Full Usage: `quote x` Parameters: x : `string` Returns: `string`	Aggiunge dei doppi-apici intorno alla stringa fornita, aggiunge dei backslash per l'escape dei backslash e dei doppi apici, e usa i codici ASCII per backquotes e caratteri non stampabili. x : `string` Returns: `string`
`quote0 x` Full Usage: `quote0 x` Parameters: x : `string` Returns: `string`	Mette degli apici singoli intorno alla stringa fornita. Non esegue alcun escape di caratteri speciali. x : `string` Returns: `string`
`repeat f x` Full Usage: `repeat f x` Parameters: f : `'a -> 'a` x : `'a` Returns: `'a`	Applica ripetutamente la funzinoe fornita a un argomento fino a quando causa un'eccezione HolFail, restituendo la manifestazione dell'argomento che causa l'eccezione. Si noti che questa non terminerà mai se la funzione non solleva mai un'eccezione. f : `'a -> 'a` x : `'a` Returns: `'a`
`report x` Full Usage: `report x` Parameters: x : `string`	Emette sullo standard output la stringa fornita come argomento preceduta dal prefisso "[HZ] " e seguita da un punto e una nuova riga. Il prefisso "[HZ] " serve a identificare i messaggi restituiti dal programma e distinguerli dai messaggi standard di .NET. x : `string`
`rev xs` Full Usage: `rev xs` Parameters: xs : `'a list` Returns: `'a list`	Inverte l'ordine degli elementi nella lista fornita. xs : `'a list` Returns: `'a list`
`rev0 ys xs` Full Usage: `rev0 ys xs` Parameters: ys : `'a list` xs : `'a list` Returns: `'a list`	Funzione tail-ricorsiva a supporto della definizione di rev ys : `'a list` xs : `'a list` Returns: `'a list`
`set_eq xs1 xs2` Full Usage: `set_eq xs1 xs2` Parameters: xs1 : `'a list` xs2 : `'a list` Returns: `bool`	Restituisce "true" sse le due liste fornite hanno gli stessi elementi (senza considerare però elementi eventuali duplicati). xs1 : `'a list` xs2 : `'a list` Returns: `bool`
`set_eq' eq xs1 xs2` Full Usage: `set_eq' eq xs1 xs2` Parameters: eq : `'a -> 'a -> bool` xs1 : `'a list` xs2 : `'a list` Returns: `bool`	Restituisce "true" sse le due liste fornite hanno gli stessi elementi (senza considerare però elementi eventuali duplicati) rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'a -> bool` xs1 : `'a list` xs2 : `'a list` Returns: `bool`
`setify xs` Full Usage: `setify xs` Parameters: xs : `'a list` Returns: `'a list`	Rimuove ogni duplicazioni di elementi dalla lista fornita. xs : `'a list` Returns: `'a list`
`setify' eq xs` Full Usage: `setify' eq xs` Parameters: eq : `'a -> 'a -> bool` xs : `'a list` Returns: `'a list`	Rimuove ogni duplicazione di elementi dalla lista fornita rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'a -> bool` xs : `'a list` Returns: `'a list`
`snd_filter p xys` Full Usage: `snd_filter p xys` Parameters: p : `'a -> bool` xys : `('b * 'a) list` Returns: `('b * 'a) list`	Elimina dalla lista di coppie fornita gli elementi con un componente destro che restituisce falso per la funzione di test fornita. p : `'a -> bool` xys : `('b * 'a) list` Returns: `('b * 'a) list`
`snd_map f xys` Full Usage: `snd_map f xys` Parameters: f : `'b -> 'c` xys : `('d * 'b) list` Returns: `('d * 'c) list`	Applica la funzione fornita al componente destro di ciascuna coppia nella lista di coppie fornita. f : `'b -> 'c` xys : `('d * 'b) list` Returns: `('d * 'c) list`
`string_of_int _arg1` Full Usage: `string_of_int _arg1` Parameters: _arg1 : `int` Returns: `string`	Restituisce la rappresentazione sotto forma di stringa dell'intero fornito _arg1 : `int` Returns: `string`
`string_variant xs0 x` Full Usage: `string_variant xs0 x` Parameters: xs0 : `string list` x : `string` Returns: `string`	Crea una variante della stringa fornita appendendo in fondo ad essa degli apostrofi fino a quando è diversa da ogni stringa all'interno della lista di stringhe da evitare fornita come argomento. Non appende alcun apostrofo se la stringa originale è già diversa da ognuna delle stringhe da evitare. xs0 : `string list` x : `string` Returns: `string`
`subset xs1 xs2` Full Usage: `subset xs1 xs2` Parameters: xs1 : `'a list` xs2 : `'a list` Returns: `bool`	Restituisce "true" sse tutti gli elementi nella prima lista fornita occorrono anche nella seconda. xs1 : `'a list` xs2 : `'a list` Returns: `bool`
`subset' eq xs1 xs2` Full Usage: `subset' eq xs1 xs2` Parameters: eq : `'a -> 'b -> bool` xs1 : `'a list` xs2 : `'b list` Returns: `bool`	Restituisce "true" sse tutti gli elementi nella prima lista fornita occorrono anche nella seconda rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'b -> bool` xs1 : `'a list` xs2 : `'b list` Returns: `bool`
`subtract xs1 xs2` Full Usage: `subtract xs1 xs2` Parameters: xs1 : `'a list` xs2 : `'a list` Returns: `'a list`	Rimuove dalla prima lista fornita gli elmenti che occorrono anche nella seconda. xs1 : `'a list` xs2 : `'a list` Returns: `'a list`
`subtract' eq xs1 xs2` Full Usage: `subtract' eq xs1 xs2` Parameters: eq : `'a -> 'b -> bool` xs1 : `'a list` xs2 : `'b list` Returns: `'a list`	Rimuove dalla prima lista fornita gli elmenti che occorrono anche nella seconda rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'b -> bool` xs1 : `'a list` xs2 : `'b list` Returns: `'a list`
`swap_arg f x y` Full Usage: `swap_arg f x y` Parameters: f : `'a -> 'b -> 'c` x : `'b` y : `'a` Returns: `'c`	Prende una funzione binaria curried, e restituisce una funzione equivalente che prende i suoi argomenti in ordine inverso. E' chiamata il combinatore 'C' nella logica combinatoria. f : `'a -> 'b -> 'c` x : `'b` y : `'a` Returns: `'c`
`switch (x, y)` Full Usage: `switch (x, y)` Parameters: x : `'a` y : `'b` Returns: `'b * 'a`	Scambia tra loro i due componenti di una coppia data. x : `'a` y : `'b` Returns: `'b * 'a`
`tl xs` Full Usage: `tl xs` Parameters: xs : `'a list` Returns: `'a list`	Funzione per estrarre da una lista fornita la sua coda. Fallisce se la lista è vuota. xs : `'a list` Returns: `'a list`
`try0 f x e` Full Usage: `try0 f x e` Parameters: f : `'a -> 'b` x : `'a` e : `Exception` Returns: `'b`	Applica la funzione fornita all'argomento fornito, e se questo causa un'eccezione HolFail allora la gestisce e solleva l'eccezione fornita come argomento al suo posto. f : `'a -> 'b` x : `'a` e : `Exception` Returns: `'b`
`try1 f x (func, msg)` Full Usage: `try1 f x (func, msg)` Parameters: f : `'a -> 'b` x : `'a` func : `string` msg : `string` Returns: `'b`	Applica la funzione fornita all'argomento fornito, e se questo causa un'eccezione HolFail allora la gestisce e solleva al suo posto un'altra eccezione HolFail con il nome di funzione e il messaggio forniti. f : `'a -> 'b` x : `'a` func : `string` msg : `string` Returns: `'b`
`try2 f x func` Full Usage: `try2 f x func` Parameters: f : `'c -> 'd` x : `'c` func : `string` Returns: `'d`	Applica la funzinoe fornita all'argomento fornito, e se questo causa un'eccezione HolFail allora la gestisce e risolleva l'HolFail con lo stesso messaggio ma per il nome di funzione fornito. f : `'c -> 'd` x : `'c` func : `string` Returns: `'d`
`try_filter f xs` Full Usage: `try_filter f xs` Parameters: f : `'a -> 'b` xs : `'a list` Returns: `'b list`	Applica la funzione fornita a quegli elementi della lista fornita che non causano un'eccezione HolFail, e rimuovendo quelli che lo fanno. f : `'a -> 'b` xs : `'a list` Returns: `'b list`
`try_find f xs` Full Usage: `try_find f xs` Parameters: f : `'a -> 'b` xs : `'a list` Returns: `'b`	Applica la funzione fornita al primo elemento della lista fornita che non causa un'eccezione HolFail. Fallisce se non c'è un tale elemento nella lista. f : `'a -> 'b` xs : `'a list` Returns: `'b`
`uncurry f (x, y)` Full Usage: `uncurry f (x, y)` Parameters: f : `'a -> 'b -> 'c` x : `'a` y : `'b` Returns: `'c`	Restituisce l'equivalente uncurried (che prende una coppia come argomento) della funzione binaria curried passata come argomento. f : `'a -> 'b -> 'c` x : `'a` y : `'b` Returns: `'c`
`unfold dest_fn x` Full Usage: `unfold dest_fn x` Parameters: dest_fn : `'a -> 'a * 'a` x : `'a` Returns: `'a list`	Usa un dato decostruttore binario per decostruire ripetutamente tutti i rami dell'argomento fornito fino a quando il decostruttore causa una HolFail exception su ciasun sotto ramo. Restituisce una lista appiattita delle estremità risultanti. dest_fn : `'a -> 'a * 'a` x : `'a` Returns: `'a list`
`unfold0 dest_fn x xs` Full Usage: `unfold0 dest_fn x xs` Parameters: dest_fn : `'a -> 'a * 'a` x : `'a` xs : `'a list` Returns: `'a list`	Funzione tail ricorsiva a supporto della definizione di unfold. dest_fn : `'a -> 'a * 'a` x : `'a` xs : `'a list` Returns: `'a list`
`unfoldl dest_fn x` Full Usage: `unfoldl dest_fn x` Parameters: dest_fn : `'a -> 'a * 'b` x : `'a` Returns: `'a * 'b list`	Usa un dato decostruttore binario per decostruire ripetutamente il ramo sinistro dell'argomento fornito fino a quando il decostruttore causa una HolFail exception. Restituisce la parte più interna sinistra accoppiata con la lista dei rami destri. dest_fn : `'a -> 'a * 'b` x : `'a` Returns: `'a * 'b list`
`unfoldl0 dest_fn x xs` Full Usage: `unfoldl0 dest_fn x xs` Parameters: dest_fn : `'a -> 'a * 'b` x : `'a` xs : `'b list` Returns: `'a * 'b list`	Funzione tail-ricorsiva a supporto della definizione di unfoldl dest_fn : `'a -> 'a * 'b` x : `'a` xs : `'b list` Returns: `'a * 'b list`
`unfoldl1 dest_fn x` Full Usage: `unfoldl1 dest_fn x` Parameters: dest_fn : `'a -> 'a * 'a` x : `'a` Returns: `'a list`	Usa un dato decostruttore binario per decostruire ripetutamente il ramo sinistro dell'argomento fornito fino a quando il decostruttore casua una HolFail Exception. Restituisce la lista che inizia con il lato sinistro più interno seguito dai rami destri. dest_fn : `'a -> 'a * 'a` x : `'a` Returns: `'a list`
`unfoldr dest_fn x` Full Usage: `unfoldr dest_fn x` Parameters: dest_fn : `'a -> 'b * 'a` x : `'a` Returns: `'b list * 'a`	Usa un dato decostruttore binario per decostruire ripetutamente il lato destro dell'argomento fornito fino a quando il decostruttore cauasa una HolFail exception. Restituisce la lista dei lati sinistri, accoppiata con il lato destro più interno. dest_fn : `'a -> 'b * 'a` x : `'a` Returns: `'b list * 'a`
`unfoldr0 dest_fn xs x` Full Usage: `unfoldr0 dest_fn xs x` Parameters: dest_fn : `'a -> 'b * 'a` xs : `'b list` x : `'a` Returns: `'b list * 'a`	dest_fn : `'a -> 'b * 'a` xs : `'b list` x : `'a` Returns: `'b list * 'a`
`unfoldr1 dest_fn x` Full Usage: `unfoldr1 dest_fn x` Parameters: dest_fn : `'a -> 'a * 'a` x : `'a` Returns: `'a list`	Usa un dato decostruttore binario per decostruire ripetutamente i rami destri dell'argomento fornito fino a quando il decostruttore causa una HolFail exception. Restituisce la lista dei lati sinistri e che finisce con il lato destro più interno. dest_fn : `'a -> 'a * 'a` x : `'a` Returns: `'a list`
`union xs1 xs2` Full Usage: `union xs1 xs2` Parameters: xs1 : `'a list` xs2 : `'a list` Returns: `'a list`	Crea una lista di elementi che occorrono in almeno una delle liste fornite. xs1 : `'a list` xs2 : `'a list` Returns: `'a list`
`union' eq xs1 xs2` Full Usage: `union' eq xs1 xs2` Parameters: eq : `'a -> 'a -> bool` xs1 : `'a list` xs2 : `'a list` Returns: `'a list`	Crea una lista di elementi che occorrono in almeno una delle liste fornite rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'a -> bool` xs1 : `'a list` xs2 : `'a list` Returns: `'a list`
`unions xss` Full Usage: `unions xss` Parameters: xss : `'a list list` Returns: `'a list`	Crea una lista di elementi che occorrono in almeno una delle liste all'interno della lista di liste fornita. xss : `'a list list` Returns: `'a list`
`unions' eq xss` Full Usage: `unions' eq xss` Parameters: eq : `'a -> 'a -> bool` xss : `'a list list` Returns: `'a list`	Crea una lista di elementi che occorrono in almeno una delle liste all'interno della lista di liste fornita rispetto a una funzione di confronto fornita come argomento. eq : `'a -> 'a -> bool` xss : `'a list list` Returns: `'a list`
`unzip xys` Full Usage: `unzip xys` Parameters: xys : `('a * 'b) list` Returns: `'a list * 'b list`	Divide la lista di coppie fornita nella lista dei primi componenti e nella lista dei secondi componenti di ciascuna coppia. xys : `('a * 'b) list` Returns: `'a list * 'b list`
`up_to m n` Full Usage: `up_to m n` Parameters: m : `int` n : `int` Returns: `int list`	Restituisce la lista degli interi crescenti contigui che partono dal primo intero fornito al secondo. Restituisce una lista vuota se il secondo argomento è minore del primo. m : `int` n : `int` Returns: `int list`
`warn x` Full Usage: `warn x` Parameters: x : `string`	Emette sullo standard output la stringa fornita come argomento preceduta dal prefisso "[HZ] Warning - " e seguita da un punto e da una nuova riga. Il prefisso "[HZ] Warning - " identifica i warning emessi dal programma. x : `string`
`zip xs ys` Full Usage: `zip xs ys` Parameters: xs : `'a list` ys : `'b list` Returns: `('a * 'b) list`	Combina in coppie gli elementi corrispondenti delle due liste fornite. Fallisce se le due liste non hanno la stessa lunghezza. xs : `'a list` ys : `'b list` Returns: `('a * 'b) list`