blob: 77016bbfe6e85ad0d2e0a631962cd7afe48c3715 (
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).
|
