|
(* 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.
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
