Commit c330aebb authored by Raphael Cauderlier's avatar Raphael Cauderlier

Remove unification tests

parent 3b33ad7c
......@@ -207,28 +207,3 @@ def unify'_aux : unify_problem -> unify_result -> unify_result.
def unify' (pb : unify_problem) :=
unify'_aux pb (unify pb).
A : sort.
f : function.
[] fol.fun_domain f --> read_sorts 2 A A.
[] fol.fun_codomain f --> A.
a : function.
[] fol.fun_domain a --> read_sorts 0.
[] fol.fun_codomain a --> A.
b : function.
[] fol.fun_domain b --> read_sorts 0.
[] fol.fun_codomain b --> A.
x : term A.
y : term A.
#SNF unify (unify_cons A x (fun_apply a) unify_nil).
#SNF unify (unify_cons A (fun_apply a) x unify_nil).
#SNF unify' (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply a) unify_nil).
#SNF unify (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply f (fun_apply a) x) unify_nil).
#SNF unify (unify_cons A x x unify_nil).
#SNF unify (unify_cons A x y unify_nil).
#SNF unify (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply f (fun_apply a) y) unify_nil).
#SNF unify' (unify_cons A (fun_apply f (fun_apply b) y) (fun_apply f y (fun_apply a)) unify_nil).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment