(* About the detection of non-dependent metas by the refine tactic *)
(* The following is a simplification of bug #2123 *)
Parameter fset : nat -> Set. Parameter widen : forall (n : nat) (s : fset n), { x : fset (S n) | s=s }. Goalforall i, fset (S i). intro.
refine (proj1_sig (widen i _)). Abort.
Messung V0.5 in Prozent
¤ 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.0.15Bemerkung:
(vorverarbeitet am 2026-09-29)
¤
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 und die Messung sind noch experimentell.
