Commit 9c60096e authored by MARCHE Claude's avatar MARCHE Claude

test for compile match

parent 191603cf
......@@ -501,7 +501,7 @@ let eliminate_algebraic_if_poly =
Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
(function
| [] -> eliminate_algebraic
| _ -> Trans.identity)
| _ -> compile_match)
let () =
Trans.register_transform "eliminate_algebraic_if_poly"
......
theory T
use import int.Int
type list = Nil | Cons int list
function tl list : list
function length (l:list) : int
(* =
match l with
| Nil -> 0
| Cons _ r -> 1 + length r
end
*)
axiom a : forall l:list. let h = tl l in length l = 1 + length h
goal g0: length (Cons 1 Nil) = 1
(*
goal g1 : forall x.
match x with A -> x=x | B A -> false | B (B _) -> false end
*)
end
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