diff options
author | 2012-06-04 12:23:14 +0200 | |
---|---|---|
committer | 2012-06-04 12:23:14 +0200 | |
commit | 86535d84cc3cffeee1dcd8545343f234e7285530 (patch) | |
tree | 9b221c283c2971f7ac151397231059e1d239e723 /plugins/dp/fol.mli | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'plugins/dp/fol.mli')
-rw-r--r-- | plugins/dp/fol.mli | 58 |
1 files changed, 0 insertions, 58 deletions
diff --git a/plugins/dp/fol.mli b/plugins/dp/fol.mli deleted file mode 100644 index 4fb763a6..00000000 --- a/plugins/dp/fol.mli +++ /dev/null @@ -1,58 +0,0 @@ - -(* Polymorphic First-Order Logic (that is Why's input logic) *) - -type typ = - | Tvar of string - | Tid of string * typ list - -type term = - | Cst of Big_int.big_int - | RCst of Big_int.big_int - | Power2 of Big_int.big_int - | Plus of term * term - | Moins of term * term - | Mult of term * term - | Div of term * term - | Opp of term - | App of string * term list - -and atom = - | Eq of term * term - | Le of term * term - | Lt of term * term - | Ge of term * term - | Gt of term * term - | Pred of string * term list - -and form = - | Fatom of atom - | Imp of form * form - | Iff of form * form - | And of form * form - | Or of form * form - | Not of form - | Forall of string * typ * form - | Exists of string * typ * form - | True - | False - -(* the integer indicates the number of type variables *) -type decl = - | DeclType of string * int - | DeclFun of string * int * typ list * typ - | DeclPred of string * int * typ list - | Axiom of string * form - -type query = decl list * form - - -(* prover result *) - -type prover_answer = - | Valid of string option - | Invalid - | DontKnow - | Timeout - | NoAnswer - | Failure of string - |