You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
(fun f -> (fun x -> f (fun v -> (x x) v)) (fun x -> f (fun v -> (x x) v)))
gives ((((a & a) -> (b | b)) -> ((a -> b) & c)) -> c) instead of (((v1 -> v0) -> ((v1 -> v0) & v2)) -> v2)
(fun f -> (fun x -> f (fun v -> (x x) v)) (fun x -> f (fun v -> (x x) v))) (fun f -> fun x -> f)
gives ((Top) -> ((Top) -> ((Top) -> (rec b = ((Top) -> (rec a = ((Top) -> (a | b)) | b)) | rec d = ((Top) -> (rec c = ((Top) -> (c | d)) | d))))))
instead of (Top -> rec v0 = (Top -> v0))
The text was updated successfully, but these errors were encountered:
Ah, I haven't updated the online version in a while. Both are correct, but the simplifier is not as powerful in the online version, so produces more verbose answers sometimes.
Speaking of not updating the online version, it looks like the online version supports let rec for terms, but I don't see any support for that in the codebase. What happened? Am I missing something?
def (used to define functions) still binds recursively, but I removed general let rec. Using let rec at arbitrary types is really tricky in a strict language. (See ocaml/ocaml#556 for some of the trouble this caused in OCaml).
(fun f -> (fun x -> f (fun v -> (x x) v)) (fun x -> f (fun v -> (x x) v)))
gives
((((a & a) -> (b | b)) -> ((a -> b) & c)) -> c)
instead of(((v1 -> v0) -> ((v1 -> v0) & v2)) -> v2)
(fun f -> (fun x -> f (fun v -> (x x) v)) (fun x -> f (fun v -> (x x) v))) (fun f -> fun x -> f)
gives
((Top) -> ((Top) -> ((Top) -> (rec b = ((Top) -> (rec a = ((Top) -> (a | b)) | b)) | rec d = ((Top) -> (rec c = ((Top) -> (c | d)) | d))))))
instead of
(Top -> rec v0 = (Top -> v0))
The text was updated successfully, but these errors were encountered: