src/HOL/ex/Antiquote.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10357 0d0cac129618
child 11586 d8a7f6318457
permissions -rw-r--r--
hide many names from Datatype_Universe.

(*  Title:      HOL/ex/Antiquote.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Simple quote / antiquote example.
*)

header {* Antiquotations *}

theory Antiquote = Main:

syntax
  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)

constdefs
  var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
  "var x env == env x"

  Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
  "Expr exp env == exp env"

parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *}
print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "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 (\<lambda>env. env x)"				(*improper*)
term "Expr (\<lambda>env. f env)"
term "Expr (\<lambda>env. f env + env x)"			(*improper*)
term "Expr (\<lambda>env. f env y z)"
term "Expr (\<lambda>env. f env + g y env)"
term "Expr (\<lambda>env. f env + g env y + h a env z)"

end