liquid-fixpoint-8.10.7: tests/proof/list01.fq

fixpoint "--rewrite"

data Vec 1 = [
  | VNil  { }
  | VCons { head : @(0), tail : Vec @(0)}
]

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)))
}

constant len: (func(1, [(Vec @(0)); int]))

match len VNil       = 0
match len VCons x xs = (1 + len xs)

constraint:
  env []
  lhs {v : int | true }
  rhs {v : int | len (VCons 1 (VCons 2 (VCons 3 VNil))) = 3}
  id 1 tag []

expand [1 : True]