Ur/Web: tests/termination.ur annotate

Coq formalization uses TDisjoint

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 24 Feb 2009 16:08:14 -0500
parents	e0ed0d4dabc9
children

rev	line source
adamc@313	1 datatype list a = Nil \| Cons of a * list a
adamc@313	2
adamc@313	3 fun isNil (t ::: Type) (ls : list t) : bool =
adamc@313	4 case ls of
adamc@313	5 Nil => True
adamc@313	6 \| Cons _ => False
adamc@313	7
adamc@313	8 fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
adamc@313	9 case ls1 of
adamc@313	10 Nil => ls2
adamc@313	11 \| Cons (x, ls1') => Cons (x, append ls1' ls2)
adamc@313	12
adamc@313	13 fun appendR (t ::: Type) (ls2 : list t) (ls1 : list t) : list t =
adamc@313	14 case ls1 of
adamc@313	15 Nil => ls2
adamc@313	16 \| Cons (x, ls1') => Cons (x, appendR ls2 ls1')
adamc@313	17
adamc@313	18 (fun naughty (t ::: Type) (ls : list t) : list t = naughty ls)
adamc@313	19
adamc@313	20 fun append1 (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
adamc@313	21 case ls1 of
adamc@313	22 Nil => ls2
adamc@313	23 \| Cons (x, ls1') => Cons (x, append2 ls2 ls1')
adamc@313	24
adamc@313	25 and append2 (t ::: Type) (ls2 : list t) (ls1 : list t) : list t =
adamc@313	26 case ls1 of
adamc@313	27 Nil => ls2
adamc@313	28 \| Cons (x, ls1') => Cons (x, append1 ls1' ls2)

Mercurial > urweb