{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/168","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/168/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/168/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/168/events","html_url":"https://github.com/FStarLang/FStar/issues/168","id":63137126,"number":168,"title":"type eq ERROR: Syntax error near line 7, character 15 in file","user":{"login":"joshjdevl","id":477053,"avatar_url":"https://avatars.githubusercontent.com/u/477053?v=3","gravatar_id":"","url":"https://api.github.com/users/joshjdevl","html_url":"https://github.com/joshjdevl","followers_url":"https://api.github.com/users/joshjdevl/followers","following_url":"https://api.github.com/users/joshjdevl/following{/other_user}","gists_url":"https://api.github.com/users/joshjdevl/gists{/gist_id}","starred_url":"https://api.github.com/users/joshjdevl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/joshjdevl/subscriptions","organizations_url":"https://api.github.com/users/joshjdevl/orgs","repos_url":"https://api.github.com/users/joshjdevl/repos","events_url":"https://api.github.com/users/joshjdevl/events{/privacy}","received_events_url":"https://api.github.com/users/joshjdevl/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":5,"created_at":"2015-03-20T01:59:31Z","updated_at":"2015-03-20T06:31:25Z","closed_at":null,"body":"```\r\nmodule OneTimePad\r\nopen Bytes\r\nopen String\r\nopen List\r\nopen Array\r\n\r\ntype eq a=x:a{|L x = R x|}\r\n```\r\n\r\nError\r\n```\r\nERROR: Syntax error near line 7, character 15 in file /tmp/fstar_VfYYdn\r\n```"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/83931554","html_url":"https://github.com/FStarLang/FStar/issues/168#issuecomment-83931554","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/168","id":83931554,"user":{"login":"joshjdevl","id":477053,"avatar_url":"https://avatars.githubusercontent.com/u/477053?v=3","gravatar_id":"","url":"https://api.github.com/users/joshjdevl","html_url":"https://github.com/joshjdevl","followers_url":"https://api.github.com/users/joshjdevl/followers","following_url":"https://api.github.com/users/joshjdevl/following{/other_user}","gists_url":"https://api.github.com/users/joshjdevl/gists{/gist_id}","starred_url":"https://api.github.com/users/joshjdevl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/joshjdevl/subscriptions","organizations_url":"https://api.github.com/users/joshjdevl/orgs","repos_url":"https://api.github.com/users/joshjdevl/repos","events_url":"https://api.github.com/users/joshjdevl/events{/privacy}","received_events_url":"https://api.github.com/users/joshjdevl/received_events","type":"User","site_admin":false},"created_at":"2015-03-20T06:31:25Z","updated_at":"2015-03-20T06:31:25Z","body":"Thank you for the feedback and links. I will try and contact the authors.\r\n\r\nHowever, I still this is quite strange. The [homepage](https://fstar-lang.org/) of FStar first sentence of the second paragraph claims that cryptographic verification can be done and the third paragraph links to Github. This is completely misleading as there is evidently no working implementation available."}}