liquid-fixpoint-0.6.0.1: tests/pos/literals02.fq

constant strLen : (func(0, [[Char]; int]))
constant len : (func(2, [(@(0)  @(1)); int]))

constant lit$cat : (Str)

distinct lit$cat : (Str)


bind 0 Data.Foldable.$36$fFoldable$91$$93$$35$$35$rlx : {VV##27 : (Data.Foldable.Foldable  fix$36$$91$$93$) | []}
bind 1 GHC.Types.True##6u : {VV##28 : bool | [(VV##28 = GHC.Types.True##6u)]}
bind 2 GHC.Types.False##68 : {VV##29 : bool | [(VV##29 = GHC.Types.False##68)]}
bind 3 GHC.Types.EQ##6U : {VV##30 : GHC.Types.Ordering | [(VV##30 = GHC.Types.EQ##6U)]}
bind 4 GHC.Types.LT##6S : {VV##31 : GHC.Types.Ordering | [(VV##31 = GHC.Types.LT##6S)]}
bind 5 GHC.Types.GT##6W : {VV##32 : GHC.Types.Ordering | [(VV##32 = GHC.Types.GT##6W)]}
bind 6 lq_anf$##1677724177##dFz : {lq_tmp$x##35 : Str | [(lq_tmp$x##35 = lit$cat)]}
bind 7 lq_anf$##1677724178##dFA : {lq_tmp$x##41 : [Char] | [(lq_tmp$x##41 ~~ lq_anf$##1677724177##dFz);
                                                            ((len lq_tmp$x##41) = (strLen lq_anf$##1677724177##dFz));
                                                            ((len lq_tmp$x##41) >= 0)]}

constraint:
  env [0; 1; 2; 3; 4; 5; 6; 7]
  lhs {VV##F##1 : int | [(VV##F##1 >= 0);
                         (VV##F##1 = (len lq_anf$##1677724178##dFA))]}
  rhs {VV##F##1 : int | [(VV##F##1 = 3)]}
  id 1 tag [1]
  // META constraint id 1 : ()