packages feed

liquid-fixpoint-0.8.10.1: tests/neg/adt2.fq

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

bind 1 x  : {v : int | true}
bind 2 y  : {v : int | true}
bind 3 xs : {v : Vec int | v = mkNil }
bind 4 ys : {v : Vec int | true}
bind 5 l1 : {v : Vec int | v = mkCons x xs }
bind 6 l2 : {v : Vec int | v = mkCons y ys }
bind 7 l3 : {v : Vec int | true }

constraint:
  env [1;3;5;7]
  lhs {v : int | l1 = l3 }
  rhs {v : int | y = head l3 }
  id 4 tag []