fixpoint "--rewrite"
define ints2 (): [int] = {
Cons 1 (Cons 2 Nil)
}
define filter (lq1 : func(0 , [a##a29r;bool]), lq2 : [a##a29r]) : [a##a29r] = {
if (isNil lq2) then Nil else (
if (lq1 (head lq2))
then (Cons (head lq2) (filter lq1 (tail lq2)))
else (filter lq1 (tail lq2)))
}
define ints0 () : [int] = {
Cons 0 (Cons 1 (Cons 2 Nil))
}
define isPos (lq1 : int) : bool = {
lq1 > 0
}
match isCons Cons x xs = (true)
match isNil Cons x xs = (false)
match isCons Nil = (false)
match isNil Nil = (true)
match tail Cons x xs = (xs)
match head Cons x xs = (x)
constant isCons : (func(1 , [[@(0)]; bool]))
constant isNil : (func(1 , [[@(0)]; bool]))
constant Nil : (func(1 , [[@(0)]]))
constant tail : (func(1 , [[@(0)];[@(0)]]))
constant head : (func(1 , [[@(0)];@(0)]))
constant ints0 : [int]
constant ints2 : [int]
constant filter : func(1 , [func(0 , [@(0); bool]);[@(0)];[@(0)]])
constant isPos : func(0 , [int; bool])
constant Cons : func(1 , [@(0);
[@(0)];
[@(0)]])
constant Nil : func(1 , [[@(0)]])
constraint:
env []
lhs {v : bool | true }
rhs {v : bool | filter isPos ints0 == ints2 }
id 1 tag []
expand [1 : True]