*To*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Monadic do notation for Isabelle*From*: Makarius <makarius at sketis.net>*Date*: Thu, 20 May 2010 19:51:10 +0200 (CEST)*In-reply-to*: <4BF44AAF.3010009@uibk.ac.at>*References*: <4BF11A08.3030604@uibk.ac.at> <AANLkTimuMcFBrcb9lNhNalOMrv8eo58W7j6ktMGR4snt@mail.gmail.com> <alpine.LNX.1.10.1005191015360.10540@atbroy100.informatik.tu-muenchen.de> <4BF44AAF.3010009@uibk.ac.at>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Wed, 19 May 2010, Christian Sternagel wrote:

* Further transformations within the type-checking phase are done by your own "check" operation, which is installed via Syntax.add_term_check1) Are those term_checks applied bottom-up to all subterms or do I have touse a recursive function that will be applied at the root?2) Further, I saw the "stage" parameter. Do I assume correctly that the stagegives the order of the checks and that type checking is done at stage 0?3) Is add_term_uncheck the symmetric operation before printing?

4) I find this framework very convenient :D. With few lines of code Iseem to have a working solution (for the parsing direction and modulothe fact that it is currently necessary to provide typing contraints atthe "right" places, but that is due to my lack of knowledge about how touse types properly in Isabelle programming).

Makarius

**Follow-Ups**:**Re: [isabelle] Monadic do notation for Isabelle***From:*Christian Sternagel

**References**:**[isabelle] Monadic do notation for Isabelle***From:*Christian Sternagel

**Re: [isabelle] Monadic do notation for Isabelle***From:*Brian Huffman

**Re: [isabelle] Monadic do notation for Isabelle***From:*Makarius

**Re: [isabelle] Monadic do notation for Isabelle***From:*Christian Sternagel

- Previous by Date: [isabelle] HOLCF and records
- Next by Date: [isabelle] WMM Call for Abstracts
- Previous by Thread: Re: [isabelle] Monadic do notation for Isabelle
- Next by Thread: Re: [isabelle] Monadic do notation for Isabelle
- Cl-isabelle-users May 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list