src/ZF/Let.thy
author paulson
Mon, 14 Aug 1995 13:42:27 +0200
changeset 1228 7d6b0241afab
parent 1094 840554ac0451
child 1401 0c439768f45c
permissions -rw-r--r--
updated version number to revision 4

(*  Title: 	ZF/Let
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1995  University of Cambridge

Let expressions, and tuple pattern-matching (borrowed from HOL)
*)

Let = FOL +

types
  letbinds  letbind

consts
  Let           :: "['a, 'a => 'b] => 'b"

syntax
  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
  ""            :: "letbind => letbinds"              ("_")
  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)

translations
  "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
  "let x = a in e"          == "Let(a, %x. e)"

defs
  Let_def       "Let(s, f) == f(s)"

end