{"action":"created","issue":{"url":"https://api.github.com/repos/Deducteam/Dedukti/issues/47","repository_url":"https://api.github.com/repos/Deducteam/Dedukti","labels_url":"https://api.github.com/repos/Deducteam/Dedukti/issues/47/labels{/name}","comments_url":"https://api.github.com/repos/Deducteam/Dedukti/issues/47/comments","events_url":"https://api.github.com/repos/Deducteam/Dedukti/issues/47/events","html_url":"https://github.com/Deducteam/Dedukti/pull/47","id":299053666,"number":47,"title":"Convertibility witness","user":{"login":"francoisthire","id":2529963,"avatar_url":"https://avatars1.githubusercontent.com/u/2529963?v=4","gravatar_id":"","url":"https://api.github.com/users/francoisthire","html_url":"https://github.com/francoisthire","followers_url":"https://api.github.com/users/francoisthire/followers","following_url":"https://api.github.com/users/francoisthire/following{/other_user}","gists_url":"https://api.github.com/users/francoisthire/gists{/gist_id}","starred_url":"https://api.github.com/users/francoisthire/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/francoisthire/subscriptions","organizations_url":"https://api.github.com/users/francoisthire/orgs","repos_url":"https://api.github.com/users/francoisthire/repos","events_url":"https://api.github.com/users/francoisthire/events{/privacy}","received_events_url":"https://api.github.com/users/francoisthire/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":7,"created_at":"2018-02-21T17:10:19Z","updated_at":"2018-02-22T21:32:29Z","closed_at":"2018-02-22T09:56:55Z","author_association":"OWNER","pull_request":{"url":"https://api.github.com/repos/Deducteam/Dedukti/pulls/47","html_url":"https://github.com/Deducteam/Dedukti/pull/47","diff_url":"https://github.com/Deducteam/Dedukti/pull/47.diff","patch_url":"https://github.com/Deducteam/Dedukti/pull/47.patch"},"body":"This is mostly an API enhancement. This PR introduces a bit of code duplication so your remarks to have a cleaner code are welcome ;)\r\n\r\nUsing the API kernel, having a witness when two terms are not convertible is very handy. This avoids going through the term looking for the witness."},"comment":{"url":"https://api.github.com/repos/Deducteam/Dedukti/issues/comments/367829212","html_url":"https://github.com/Deducteam/Dedukti/pull/47#issuecomment-367829212","issue_url":"https://api.github.com/repos/Deducteam/Dedukti/issues/47","id":367829212,"user":{"login":"fblanqui","id":10852505,"avatar_url":"https://avatars2.githubusercontent.com/u/10852505?v=4","gravatar_id":"","url":"https://api.github.com/users/fblanqui","html_url":"https://github.com/fblanqui","followers_url":"https://api.github.com/users/fblanqui/followers","following_url":"https://api.github.com/users/fblanqui/following{/other_user}","gists_url":"https://api.github.com/users/fblanqui/gists{/gist_id}","starred_url":"https://api.github.com/users/fblanqui/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fblanqui/subscriptions","organizations_url":"https://api.github.com/users/fblanqui/orgs","repos_url":"https://api.github.com/users/fblanqui/repos","events_url":"https://api.github.com/users/fblanqui/events{/privacy}","received_events_url":"https://api.github.com/users/fblanqui/received_events","type":"User","site_admin":false},"created_at":"2018-02-22T21:32:29Z","updated_at":"2018-02-22T21:32:29Z","author_association":"CONTRIBUTOR","body":"Isn't it the other way: w_1 is a subterm of a term convertible to t_1? \nMore precisely: w_1 is a subterm of a reduct of t_1? It looks more \ninformative to me.\n\n\nLe 22/02/2018 à 21:27, fthire a écrit :\n>\n>     Then, you just have to give the types of variables too.\n>     Yeah, a typed-context actually that is useful only for this purpose.\n>\n>     But what if you realize that two terms are not convertible after\n>     having /reduced/ them? They are not subterms of your initial terms\n>     anymore.\n>\n> Yeah, that is exactly what I said I think. w_1 is not a subterm of t_1 \n> but convertible to a subterm of t_1. This is not a problem in general \n> because if you use this function, you precisely know the congruence \n> relation.\n>\n> —\n> You are receiving this because you commented.\n> Reply to this email directly, view it on GitHub \n> <https://github.com/Deducteam/Dedukti/pull/47#issuecomment-367811130>, \n> or mute the thread \n> <https://github.com/notifications/unsubscribe-auth/AKWYmZwKVf9HqIhY4ZPOx6vlNkxfQ4o1ks5tXc2agaJpZM4SOALZ>.\n>\n\n"}}
{"actor":{"display_login":"fblanqui"}}