packages feed

liquid-fixpoint-0.8.0.2: tests/pos/literals01.fq

constant lit$cat : (Str)
distinct lit$cat : (Str)

constraint:
  env []
  lhs {v : Str | v = lit$cat }
  rhs {v : Str | strLen v = 3 }
  id 1 tag [6]

constraint:
  env []
  lhs {v : Str | v = lit$cat }
  rhs {v : Str | v = "cat"   }
  id 2 tag [6]