{"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/comments/12730062","html_url":"https://github.com/FStarLang/FStar/commit/f24ee3b327ec6e387eea343aee8e860d54626cba#commitcomment-12730062","id":12730062,"user":{"login":"aa755msr","id":12737628,"avatar_url":"https://avatars.githubusercontent.com/u/12737628?v=3","gravatar_id":"","url":"https://api.github.com/users/aa755msr","html_url":"https://github.com/aa755msr","followers_url":"https://api.github.com/users/aa755msr/followers","following_url":"https://api.github.com/users/aa755msr/following{/other_user}","gists_url":"https://api.github.com/users/aa755msr/gists{/gist_id}","starred_url":"https://api.github.com/users/aa755msr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/aa755msr/subscriptions","organizations_url":"https://api.github.com/users/aa755msr/orgs","repos_url":"https://api.github.com/users/aa755msr/repos","events_url":"https://api.github.com/users/aa755msr/events{/privacy}","received_events_url":"https://api.github.com/users/aa755msr/received_events","type":"User","site_admin":false},"position":12,"line":43,"path":"examples/low-level/huffman/huffman.fst","commit_id":"f24ee3b327ec6e387eea343aee8e860d54626cba","created_at":"2015-08-17T01:45:08Z","updated_at":"2015-08-17T01:45:08Z","body":"This is defined here :\r\nhttps://github.com/FStarLang/FStar/blob/92c029b31da795c95658b75b5d34feb346490905/examples/low-level/stackAndHeap.fst#L462"}}