Goal True.
evar (p : bool).
unify ?p true. let v := eval vm_compute in (orb p false) in match v with true => idtacend. assert (orb p false = true).
vm_compute. matchgoalwith |- true = _ => idtacend.
easy.
easy. Qed.
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.