liquid-fixpoint-0.9.6.3.1: tests/pos/literals04.fq
constant lit$year : (Str)
constant lit$title : (Str)
constant lit$star : (Str)
constant lit$director : (Str)
constant listElts : (func(0, [LLChar; (Set_Set Str)]))
constant Set_sng : (func(1, [@(0); (Set_Set @(0))]))
bind 1 a : {a : Str | a == "director" }
bind 2 things : {v : LLChar | (listElts v ~~ (Set_cup (Set_sng lit$year) (Set_cup (Set_sng lit$star) (Set_cup (Set_sng lit$director) (Set_sng lit$title)))))}
constraint:
env [ 1; 2 ]
lhs {v : int | true }
rhs {v : int | Set_mem a (listElts things)}
id 1 tag []