liquid-fixpoint-0.7.0.1: tests/neg/adt_bin_0.fq

constant prop : func(2, [@(0); @(1)])
constant gibber : func(0, [int; int; int])


// constant prop : func(0, [Binary; Bin])

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

data Binary 0 = [
  | mkB0 { }
  | mkB1 { }
]

bind 0 n : {n:Int | gibber 2 3 = 4 }
bind 1 p : {p:Binary | prop p = mkBin n && prop p = mkBin 0}
bind 2 p : {p:Binary | prop p = mkBin n && prop p = mkBin 1}

constraint:
  env [0; 1]
  lhs {v:int | true}
  rhs {v:int | n == 0 || n == 1}
  id 1 tag []

constraint:
  env [0; 2]
  lhs {v:int | true}
  rhs {v:int | n == 0 }
  id 2 tag []