{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/1438","repository_url":"https://api.github.com/repos/FStarLang/FStar","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/1438/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/1438/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/1438/events","html_url":"https://github.com/FStarLang/FStar/issues/1438","id":317141219,"number":1438,"title":"(Error 37) Constructor ML not found","user":{"login":"natzei","id":4339506,"avatar_url":"https://avatars3.githubusercontent.com/u/4339506?v=4","gravatar_id":"","url":"https://api.github.com/users/natzei","html_url":"https://github.com/natzei","followers_url":"https://api.github.com/users/natzei/followers","following_url":"https://api.github.com/users/natzei/following{/other_user}","gists_url":"https://api.github.com/users/natzei/gists{/gist_id}","starred_url":"https://api.github.com/users/natzei/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/natzei/subscriptions","organizations_url":"https://api.github.com/users/natzei/orgs","repos_url":"https://api.github.com/users/natzei/repos","events_url":"https://api.github.com/users/natzei/events{/privacy}","received_events_url":"https://api.github.com/users/natzei/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-04-24T09:22:58Z","updated_at":"2018-04-24T15:03:32Z","closed_at":null,"author_association":"NONE","body":"I'm trying F* at http://fstar-lang.org/tutorial/. However, the basic examples in the introduction return the error `(Error 37) Constructor ML not found`.\r\n\r\nFor example\r\n```ocaml\r\ntype filename = string\r\n\r\n(** [canWrite] is a function specifying whether a file [f] can be written *)\r\nlet canWrite (f:filename) = \r\n  match f with \r\n    | \"demo/tempfile\" -> true\r\n    | _ -> false\r\n\r\n(** [canRead] is also a function ... *)\r\nlet canRead (f:filename) = \r\n  canWrite f               (* writeable files are also readable *)\r\n  || f=\"demo/README\"       (* and so is demo/README *)\r\n  \r\nval read  : f:filename{canRead f}  -> ML string\r\nlet read f  = FStar.IO.print_string (\"Dummy read of file \" ^ f ^ \"\\n\"); f\r\n\r\nval write : f:filename{canWrite f} -> string -> ML unit\r\nlet write f s = FStar.IO.print_string (\"Dummy write of string \" ^ s ^ \" to file \" ^ f ^ \"\\n\")\r\n\r\nlet passwd : filename = \"demo/password\"\r\nlet readme : filename = \"demo/README\"\r\nlet tmp    : filename = \"demo/tempfile\"\r\n\r\nval staticChecking : unit -> ML unit\r\nlet staticChecking () =\r\n  let v1 = read tmp in\r\n  let v2 = read readme in\r\n  (* let v3 = read passwd in // invalid read, fails type-checking *)\r\n  write tmp \"hello!\"\r\n  (* ; write passwd \"junk\" // invalid write , fails type-checking *)\r\n```"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/383966387","html_url":"https://github.com/FStarLang/FStar/issues/1438#issuecomment-383966387","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/1438","id":383966387,"user":{"login":"A-Manning","id":10554686,"avatar_url":"https://avatars1.githubusercontent.com/u/10554686?v=4","gravatar_id":"","url":"https://api.github.com/users/A-Manning","html_url":"https://github.com/A-Manning","followers_url":"https://api.github.com/users/A-Manning/followers","following_url":"https://api.github.com/users/A-Manning/following{/other_user}","gists_url":"https://api.github.com/users/A-Manning/gists{/gist_id}","starred_url":"https://api.github.com/users/A-Manning/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/A-Manning/subscriptions","organizations_url":"https://api.github.com/users/A-Manning/orgs","repos_url":"https://api.github.com/users/A-Manning/repos","events_url":"https://api.github.com/users/A-Manning/events{/privacy}","received_events_url":"https://api.github.com/users/A-Manning/received_events","type":"User","site_admin":false},"created_at":"2018-04-24T15:03:32Z","updated_at":"2018-04-24T15:03:32Z","author_association":"CONTRIBUTOR","body":"Do you have `FStar.All` open? The `ML` effect is defined there, so you need to add `open FStar.All` to your module, or change `ML` to `All.ML`. "}}
{"actor":{"display_login":"A-Manning"}}