src/ZF/Let.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 4879 58656c6a3551
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/Let
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 
     6 Let expressions, and tuple pattern-matching (borrowed from HOL)
     7 *)
     8 
     9 Let = FOL +
    10 
    11 types
    12   letbinds  letbind
    13 
    14 consts
    15   Let           :: ['a, 'a => 'b] => 'b
    16 
    17 syntax
    18   "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
    19   ""            :: letbind => letbinds              ("_")
    20   "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
    21   "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
    22 
    23 translations
    24   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
    25   "let x = a in e"          == "Let(a, %x. e)"
    26 
    27 defs
    28   Let_def       "Let(s, f) == f(s)"
    29 
    30 end