(* Author: Florian Haftmann, TU Muenchen *)
section \<open>Pretty syntax for lattice operations\<close>
theory Lattice_Syntax
imports Main
begin
notation
bot ("\") and
top ("\") and
inf (infixl "\" 70) and
sup (infixl "\" 65) and
Inf ("\ _" [900] 900) and
Sup ("\ _" [900] 900)
syntax
"_INF1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
"_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
"_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|