packages feed

liquid-fixpoint-0.9.6.3.2: tests/pos/ext_lam_multi.fq

fixpoint "--rewrite"
fixpoint "--extensionality"
fixpoint "--allowho"

constant f : (func(0 , [int; int; int]))
define f (x : int, y : int) : int = {(13)}

expand [1 : True]

constraint:
  env []
  lhs {VV1 : Tuple | true }
  rhs {VV2 : Tuple | (f = \y : int -> \k : int -> 13) }
  id 1 tag []