src/HOLCF/ex/Loop.thy
author regensbu
Thu Jun 29 16:28:40 1995 +0200 (1995-06-29)
changeset 1168 74be52691d62
parent 1150 66512c9e6bd6
child 1274 ea0668a1c0ba
permissions -rw-r--r--
The curried version of HOLCF is now just called HOLCF. The old
uncurried version is no longer supported
nipkow@244
     1
(*  Title:	HOLCF/ex/loop.thy
nipkow@244
     2
    ID:         $Id$
nipkow@244
     3
    Author: 	Franz Regensburger
nipkow@244
     4
    Copyright	1993 Technische Universitaet Muenchen
nipkow@244
     5
nipkow@244
     6
Theory for a loop primitive like while
nipkow@244
     7
*)
nipkow@244
     8
nipkow@244
     9
Loop = Tr2 +
nipkow@244
    10
nipkow@244
    11
consts
nipkow@244
    12
nipkow@244
    13
	step  :: "('a -> tr)->('a -> 'a)->'a->'a"
nipkow@244
    14
	while :: "('a -> tr)->('a -> 'a)->'a->'a"
nipkow@244
    15
regensbu@1168
    16
defs
nipkow@244
    17
regensbu@1168
    18
  step_def	"step == (LAM b g x. If b`x then g`x else x fi)"
regensbu@1168
    19
  while_def	"while == (LAM b g. fix`(LAM f x.
regensbu@1168
    20
                   If b`x then f`(g`x) else x fi))"
nipkow@244
    21
nipkow@244
    22
end
nipkow@244
    23