{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/277","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/277/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/277/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/277/events","html_url":"https://github.com/FStarLang/FStar/issues/277","id":93086568,"number":277,"title":"Shouldn't extract lemmas and ghost things in general","user":{"login":"catalin-hritcu","id":5850655,"avatar_url":"https://avatars.githubusercontent.com/u/5850655?v=3","gravatar_id":"","url":"https://api.github.com/users/catalin-hritcu","html_url":"https://github.com/catalin-hritcu","followers_url":"https://api.github.com/users/catalin-hritcu/followers","following_url":"https://api.github.com/users/catalin-hritcu/following{/other_user}","gists_url":"https://api.github.com/users/catalin-hritcu/gists{/gist_id}","starred_url":"https://api.github.com/users/catalin-hritcu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/catalin-hritcu/subscriptions","organizations_url":"https://api.github.com/users/catalin-hritcu/orgs","repos_url":"https://api.github.com/users/catalin-hritcu/repos","events_url":"https://api.github.com/users/catalin-hritcu/events{/privacy}","received_events_url":"https://api.github.com/users/catalin-hritcu/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/FStarLang/FStar/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-07-05T07:22:47Z","updated_at":"2015-07-21T05:10:20Z","closed_at":null,"body":"We had issues extracting RPC to OCaml because it uses some assumed lemmas, and those uses get compiled down to calls in OCaml, but then there is nothing to link against because they are just assumed. Needed to remove the assume and instead admit their body ...\r\n\r\nIn general, we shouldn't extract lemmas and ghost things.\r\n"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/123162299","html_url":"https://github.com/FStarLang/FStar/issues/277#issuecomment-123162299","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/277","id":123162299,"user":{"login":"nikswamy","id":6163359,"avatar_url":"https://avatars.githubusercontent.com/u/6163359?v=3","gravatar_id":"","url":"https://api.github.com/users/nikswamy","html_url":"https://github.com/nikswamy","followers_url":"https://api.github.com/users/nikswamy/followers","following_url":"https://api.github.com/users/nikswamy/following{/other_user}","gists_url":"https://api.github.com/users/nikswamy/gists{/gist_id}","starred_url":"https://api.github.com/users/nikswamy/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nikswamy/subscriptions","organizations_url":"https://api.github.com/users/nikswamy/orgs","repos_url":"https://api.github.com/users/nikswamy/repos","events_url":"https://api.github.com/users/nikswamy/events{/privacy}","received_events_url":"https://api.github.com/users/nikswamy/received_events","type":"User","site_admin":false},"created_at":"2015-07-21T05:10:20Z","updated_at":"2015-07-21T05:10:20Z","body":"Yes, this is very much among the things we are addressing in --codegen\r\nOCaml-experimental"}}