Definition foo{A}(a b: nat)(k: nat -> A): A :=
k (a + b).
Definition bar{A}(a b: nat)(k: nat -> A): A :=
k (a - b).
Notation"'let/c' x := r 'in' b" := (r (fun x => b))
(x binder, at level 200, right associativity,
format "'[hv' 'let/c' x := r 'in' '//' b ']'").
Definition chain(x y: nat): Prop := let/c f := foo x y in let/c b := bar x y in
f = b.
Print chain.
Messung V0.5
¤ 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.10Bemerkung:
(vorverarbeitet)
¤
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.
