| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/ex/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle Antiquote.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/ex/Antiquote.thy Author: Markus Wenzel, TU Muenchen *) section ‹Antiquotations› theory Antiquote imports Main begin text ‹A simple example on quote / antiquote in higher-order abstract syntax.› definition Expr :: "(('a → nat) → nat) → ('a → nat) → nat" where "Expr exp env = exp env" syntax "_Expr" :: "'a → 'a" (‹(‹notation=‹prefix EXPR››EXPR _)› [1000] 999) "_Var" :: "'a → ('a → nat) → nat" (‹(‹notation=‹prefix VAR››VAR _)› [1000] 999) syntax_consts "_Expr" ⇌ Expr parse_translation ‹[Syntax_Trans.quote_antiquote_tr syntax_const‹_Expr› syntax_const‹_Var› const_syntax‹Expr›]› print_translation ‹[Syntax_Trans.quote_antiquote_tr' syntax_const‹_Expr› syntax_const‹_Var› const_syntax‹Expr›]› term "EXPR (a + b + c)" term "EXPR (a + b + c + VAR x + VAR y + 1)" term "EXPR (VAR (f w) + VAR x)" term "Expr (λenv. env x)" ― ‹improper› term "Expr (λenv. f env)" term "Expr (λenv. f env + env x)" ― ‹improper› term "Expr (λenv. f env y z)" term "Expr (λenv. f env + g y env)" term "Expr (λenv. f env + g env y + h a env z)" end
¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-06-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-11