blob: f106a64cb5e5a1daab4966e537d83e1a77611f44 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* Test of inference of elimination predicate for "if" *)
(* submitted by Robert R Schneck *)
Axiom bad : false = true.
Definition try1 : False :=
match bad in (_ = b) return (if b then False else True) with
| refl_equal => I
end.
Definition try2 : False :=
match bad in (_ = b) return ((if b then False else True):Prop) with
| refl_equal => I
end.
Definition try3 : False :=
match
bad in (_ = b) return ((fun b' : bool => if b' then False else True) b)
with
| refl_equal => I
end.
|
