From 40626d5b73d1eefdde923c80530fec20ff3880d6 Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 14 Jul 2017 10:28:09 +0200 Subject: [PATCH] New failing problem, which shows that we need to change special_k --- ocaml/problems.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/ocaml/problems.ml b/ocaml/problems.ml index f586c5d..ca3a0d0 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -398,7 +398,20 @@ solve_many [ ]*) ];; -(*failwith "OKAy";;*) +(* This now fails *) +solve (problem_of + (Some"x PAC PAC PAC PAC PAC a") + ["x PAC PAC PAC PAC PAC b"] + ["y x"; "y z"] + (* In general: + DIV x (n times PAC) a + CON x (n times PAC) b + 1 y (m times lambda. x) 0 + 2 y z 0 + when x steps on the n+1-th argument, + y must apply n+m+1 variables + Thus special_k must be >=n+m+1 *) +);; solve_many ([ p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ; -- 2.39.2