blob: ce9a0ecb4ad76ea4d0976ce354f182d76cf21f61 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(**********************************************************************)
(* Test dependencies in constructors *)
(**********************************************************************)
Check
(fun x : {b : bool | if b then True else False} =>
match x return (let (b, _) := x in if b then True else False) with
| exist _ true y => y
| exist _ false z => z
end).
|
