liquid-fixpoint-0.7.0.3: tests/proof/list00.fq

fixpoint "--rewrite"

constant len: (func(1, [(Main.List  @(0)); int]))
constant Cons: (func(2, [@(0); (Main.List  @(0)); (Main.List @(0))]))
constant Nil: (Main.List @(0))

match len Nil = 0
match len Cons x xs = (1 + len xs)

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

expand [1 : True]