|
(* Check if omission of "as" in return clause works w/ section variables too *)
Section sec.
Variable b: bool.
Definition d' :=
(match b return b = true \/ b = false with
| true => or_introl _ (refl_equal true)
| false => or_intror _ (refl_equal false)
end).
End sec.
¤ Dauer der Verarbeitung: 0.20 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.
|
