1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* Checking computation of free vars of a term for generalization *)
Definition Decision := fun P : Prop => {P} + {~ P}.
Class SetUnfold (P Q : Prop) : Prop := Build_SetUnfold { set_unfold : P <-> Q
}.
Section Filter_Help.
Context {A: Type}.
Context (fold_right : forall A B : Type, (B -> A -> A) -> A -> list B -> A).
Definition lType2 := (sigT (fun (P : A -> Prop) => forall a, Decision (P
a))).
Definition test (X: lType2) := let (x, _) := X in x.
Global Instance foo `{fhl1 : list lType2} m Q:
SetUnfold (Q)
(fold_right _ _ (fun (s : lType2) => let (P, _) := s in and (P
m)) (Q) (fhl1)).
Abort.
End Filter_Help.
|
