liquid-fixpoint-0.7.0.1: tests/pos/adt_bin_lam.fq

fixpoint "--allowho"

data Bin 0 = [
  | mkBin { nBin : Int }
]

bind 0 b  : {b : Bin | true}
bind 1 g1 : {g1 : func(0, [int; Bin]) | g1 = (\x:int -> b) }
bind 2 g2 : {g2 : func(0, [bool; Bin]) | g2 = (\x:bool -> b) }
bind 3 f  : {f:func(0, [Bin; Bin]) | f = (\x:Bin -> b) }

constraint:
  env [0; 1; 2; 3]
  lhs {v:int | f b == b }
  rhs {v:int | b == f b }
  id 1 tag []