parse_translation‹
let
fun antiquote_tr i (Const (syntax_const‹_antiquote›, _) $
(t as Const (syntax_const‹_antiquote›, _) $ _)) = skip_antiquote_tr i t
| antiquote_tr i (Const (syntax_const‹_antiquote›, _) $ t) =
antiquote_tr i t $ Bound i
| antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
| antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
| antiquote_tr _ a = a
and skip_antiquote_tr i ((c as Const (syntax_const‹_antiquote›, _)) $ t) =
c $ skip_antiquote_tr i t
| skip_antiquote_tr i t = antiquote_tr i t;
fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
| quote_tr ts = raise TERM ("quote_tr", ts);
in [(syntax_const‹_quote›, K quote_tr)] end ›
text‹basic examples› term"«a + b + c¬" term"«a + b + c + 🚫x + 🚫y + 1¬" term"«🚫(f w) + 🚫x¬" term"«f 🚫x 🚫y z¬"
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.
