Commit 4a1ccfbe authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

No commit message

No commit message
parent 7351635f
theory Test
inductive p(int) =
| A : p(0) -> true
end
theory Test
inductive p(int) =
| A : (p(0) -> true) -> p(0)
end
theory Test
inductive p(int) =
| A : 0=0
end
......@@ -973,7 +973,7 @@ let rec check_unquantified_clausal_form loc ps f = match f.f_node with
(* TODO: vrifier galement que les arguments de ps' ont exactement
les mmes types que ceux de la dclaration de ps (et non plus
prcis) *)
if ps.ls_name != ps.ls_name then
if ps'.ls_name != ps.ls_name then
errorm ~loc "head of clause does not contain the inductive predicate"
| _ ->
errorm ~loc "this case is not in clausal form"
......
(* test file *)
theory A
end
theory B
use import A
end
theory C
use A
use B
end
theory Test
type 'a list = Nil | Cons('a, 'a list)
inductive even_length('a list) =
| Even_nil : even_length(Nil : int list)
| Even_cons: forall x,y:'a, l:'a list.
even_length(l) -> even_length(Cons(x,Cons(y,l)))
lemma Ax : even_length(Cons(1,Cons(2,Nil)))
inductive p(int) =
| A : 0=0
end
theory TestPrelude
......
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