The negation normal form function

The negation normal form function is written in the TWB as the following Ocaml function: source Pc let neg = function formula ( a ) -> formula ( ~ a ) let rec nnf = function |formula ( a & b ) -> formula ( {nnf a} & {nnf b} ) |formula ( ~ ( a & b ) ) -> formula ( {nnf formula ( ~ a )} v {nnf formula ( ~ b )} ) |formula ( a v b ) -> formula ({nnf a} v {nnf b}) |formula ( ~ ( a v b ) ) -> formula ( {nnf formula ( ~ a )} & {nnf formula ( ~ b )} ) |formula ( a <-> b ) -> formula ( {nnf formula ( a -> b )} & {nnf formula ( b -> a )} ) |formula ( ~ ( a <-> b ) ) -> formula ( {nnf formula ( ~ (a -> b) )} v {nnf formula ( ~ (b -> a) )} ) |formula ( a -> b ) -> nnf formula ( (~ a) v b ) |formula ( ~ (a -> b) ) -> nnf formula ( a & (~ b) ) |formula ( ~ ~ a ) -> nnf a |formula (Verum) -> formula (Verum) |formula (Falsum) -> formula (Falsum) |formula (~ Verum) -> formula (Falsum) |formula (~ Falsum) -> formula (Verum) |formula ( ~ A ) as f -> f | _ as f -> f We assume this function to be in a file pclib.ml. The file is then included in the the main logic module by using the directive Open Pclib.