Translation from Ocaml to Haskell of John Harrison's ATP code.
This package is a liberal translation from OCaml to Haskell of the automated theorem prover written in OCaml in John Harrison's book "Practical Logic and Automated Reasoning". Click on module ATP below for an overview.
1.14.3aarch64-darwinaarch64-freebsdaarch64-genodeaarch64-linuxaarch64-netbsdaarch64-noneaarch64-windowsaarch64_be-nonearm-nonearmv5tel-linuxarmv6l-linuxarmv6l-netbsdarmv6l-nonearmv7a-darwinarmv7a-linuxarmv7a-netbsdarmv7l-linuxarmv7l-netbsdavr-nonei686-cygwini686-darwini686-freebsdi686-genodei686-linuxi686-netbsdi686-nonei686-openbsdi686-windowsjavascript-ghcjsloongarch64-linuxm68k-linuxm68k-netbsdm68k-nonemicroblaze-linuxmicroblaze-nonemicroblazeel-linuxmicroblazeel-nonemips-linuxmips-nonemips64-linuxmips64-nonemips64el-linuxmipsel-linuxmipsel-netbsdmmix-mmixwaremsp430-noneor1k-nonepowerpc-netbsdpowerpc-nonepowerpc64-linuxpowerpc64le-linuxpowerpcle-noneriscv32-linuxriscv32-netbsdriscv32-noneriscv64-linuxriscv64-netbsdriscv64-nonerx-nones390-linuxs390-nones390x-linuxs390x-nonevc4-nonewasm32-wasiwasm64-wasix86_64-cygwinx86_64-darwinx86_64-freebsdx86_64-genodex86_64-linuxx86_64-netbsdx86_64-nonex86_64-openbsdx86_64-redoxx86_64-solarisx86_64-windows