Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 2 kB

Quellcode-Bibliothek Monad_Syntax.thy Sprache: Isabelle

(*  Title:      HOL/Library/Monad_Syntax.thy
    Author:     Alexander Krauss, TU Muenchen
    Author:     Christian Sternagel, University of Innsbruck
*)

section \<open>Monad notation for arbitrary types\<close>

theory Monad_Syntax
  imports Main
begin

text \<open>
We provide a convenient do-notation for monadic expressions well-known from Haskell.
\<^const>\<open>Let\<close> is printed specially in do-expressions.
\<close>

consts
  bind :: "'a \ ('b \ 'c) \ 'd" (infixl \\\ 54)

notation (ASCII)
  bind (infixl \<open>>>=\<close> 54)

abbreviation (do_notation)
  bind_do :: "'a \ ('b \ 'c) \ 'd"
  where "bind_do \ bind"

notation (output)
  bind_do (infixl \<open>\<bind>\<close> 54)

notation (ASCII output)
  bind_do (infixl \<open>>>=\<close> 54)

nonterminal do_binds and do_bind
syntax
  "_do_block" :: "do_binds \ 'a"
    (\<open>(\<open>open_block notation=\<open>mixfix do block\<close>\<close>do {//(2  _)//})\<close> [12] 62)
  "_do_bind"  :: "[pttrn, 'a] \ do_bind"
    (\<open>(\<open>indent=2 notation=\<open>infix do bind\<close>\<close>_ \<leftarrow>/ _)\<close> 13)
  "_do_let" :: "[pttrn, 'a] \ do_bind"
    (\<open>(\<open>indent=2 notation=\<open>infix do let\<close>\<close>let _ =/ _)\<close> [1000, 13] 13)
  "_do_then" :: "'a \ do_bind" (\_\ [14] 13)
  "_do_final" :: "'a \ do_binds" (\_\)
  "_do_cons" :: "[do_bind, do_binds] \ do_binds"
    (\<open>(\<open>open_block notation=\<open>infix do next\<close>\<close>_;//_)\<close> [13, 12] 12)
  "_thenM" :: "['a, 'b] \ 'c" (infixl \\\ 54)

syntax (ASCII)
  "_do_bind" :: "[pttrn, 'a] \ do_bind"
    (\<open>(\<open>indent=2 notation=\<open>infix do bind\<close>\<close>_ <-/ _)\<close> 13)
  "_thenM" :: "['a, 'b] \ 'c" (infixl \>>\ 54)

syntax_consts
  "_do_block" "_do_cons" "_do_bind" "_do_then" \<rightleftharpoons> bind and
  "_do_let" \<rightleftharpoons> Let

translations
  "_do_block (_do_cons (_do_then t) (_do_final e))"
    \<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
  "_do_block (_do_cons (_do_bind p t) (_do_final e))"
    \<rightleftharpoons> "CONST bind_do t (\<lambda>p. e)"
  "_do_block (_do_cons (_do_let p t) bs)"
    \<rightleftharpoons> "let p = t in _do_block bs"
  "_do_block (_do_cons b (_do_cons c cs))"
    \<rightleftharpoons> "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
  "_do_cons (_do_let p t) (_do_final s)"
    \<rightleftharpoons> "_do_final (let p = t in s)"
  "_do_block (_do_final e)" \<rightharpoonup> "e"
  "(m \ n)" \ "(m \ (\_. n))"

adhoc_overloading
  bind \<rightleftharpoons> Set.bind Predicate.bind Option.bind List.bind

end

quality82%

¤ 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.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.