packages feed

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 []