{"action":"created","issue":{"url":"https://api.github.com/repos/jonsterling/JonPRL/issues/234","labels_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/234/labels{/name}","comments_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/234/comments","events_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/234/events","html_url":"https://github.com/jonsterling/JonPRL/pull/234","id":105475895,"number":234,"title":"Simplified inconsistent DecideEq rule","user":{"login":"jozefg","id":814961,"avatar_url":"https://avatars.githubusercontent.com/u/814961?v=3","gravatar_id":"","url":"https://api.github.com/users/jozefg","html_url":"https://github.com/jozefg","followers_url":"https://api.github.com/users/jozefg/followers","following_url":"https://api.github.com/users/jozefg/following{/other_user}","gists_url":"https://api.github.com/users/jozefg/gists{/gist_id}","starred_url":"https://api.github.com/users/jozefg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jozefg/subscriptions","organizations_url":"https://api.github.com/users/jozefg/orgs","repos_url":"https://api.github.com/users/jozefg/repos","events_url":"https://api.github.com/users/jozefg/events{/privacy}","received_events_url":"https://api.github.com/users/jozefg/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-09-08T21:43:54Z","updated_at":"2015-09-08T21:55:18Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/jonsterling/JonPRL/pulls/234","html_url":"https://github.com/jonsterling/JonPRL/pull/234","diff_url":"https://github.com/jonsterling/JonPRL/pull/234.diff","patch_url":"https://github.com/jonsterling/JonPRL/pull/234.patch"},"body":"This is one fix for #233. Instead of taking this `C` parameter we don't do that and instead just force the user to prove that each branch is equal at `T`.\r\n\r\nThis should be fine though because we give them this assumption of equality so in theory they can use that to vary `T` depending on what branch they're proving things in. "},"comment":{"url":"https://api.github.com/repos/jonsterling/JonPRL/issues/comments/138715337","html_url":"https://github.com/jonsterling/JonPRL/pull/234#issuecomment-138715337","issue_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/234","id":138715337,"user":{"login":"jozefg","id":814961,"avatar_url":"https://avatars.githubusercontent.com/u/814961?v=3","gravatar_id":"","url":"https://api.github.com/users/jozefg","html_url":"https://github.com/jozefg","followers_url":"https://api.github.com/users/jozefg/followers","following_url":"https://api.github.com/users/jozefg/following{/other_user}","gists_url":"https://api.github.com/users/jozefg/gists{/gist_id}","starred_url":"https://api.github.com/users/jozefg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jozefg/subscriptions","organizations_url":"https://api.github.com/users/jozefg/orgs","repos_url":"https://api.github.com/users/jozefg/repos","events_url":"https://api.github.com/users/jozefg/events{/privacy}","received_events_url":"https://api.github.com/users/jozefg/received_events","type":"User","site_admin":false},"created_at":"2015-09-08T21:55:18Z","updated_at":"2015-09-08T21:55:18Z","body":"Here's a quick demonstration of handling dependence with this rule\r\n\r\n```\r\nTheorem not-uhoh : [\r\n  (x : unit + void) member(decide(x; a.a; b.b); decide(x; a.unit; b.void))\r\n] {\r\n  auto; eq-cd [unit, void]; auto;\r\n\r\n  hyp-subst → <eq> [h.=(_; _; decide(h; _._; _._))];\r\n  aux { elim #4; reduce; auto };\r\n\r\n  reduce; auto\r\n}.\r\n```"}}