{"action":"created","issue":{"url":"https://api.github.com/repos/snu-sf-class/pl2016/issues/60","repository_url":"https://api.github.com/repos/snu-sf-class/pl2016","labels_url":"https://api.github.com/repos/snu-sf-class/pl2016/issues/60/labels{/name}","comments_url":"https://api.github.com/repos/snu-sf-class/pl2016/issues/60/comments","events_url":"https://api.github.com/repos/snu-sf-class/pl2016/issues/60/events","html_url":"https://github.com/snu-sf-class/pl2016/issues/60","id":147960181,"number":60,"title":"Assignment 06. P11.v . Error: Tactic failure.","user":{"login":"k32l","id":7943961,"avatar_url":"https://avatars.githubusercontent.com/u/7943961?v=3","gravatar_id":"","url":"https://api.github.com/users/k32l","html_url":"https://github.com/k32l","followers_url":"https://api.github.com/users/k32l/followers","following_url":"https://api.github.com/users/k32l/following{/other_user}","gists_url":"https://api.github.com/users/k32l/gists{/gist_id}","starred_url":"https://api.github.com/users/k32l/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/k32l/subscriptions","organizations_url":"https://api.github.com/users/k32l/orgs","repos_url":"https://api.github.com/users/k32l/repos","events_url":"https://api.github.com/users/k32l/events{/privacy}","received_events_url":"https://api.github.com/users/k32l/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-04-13T06:32:31Z","updated_at":"2016-04-13T09:06:19Z","closed_at":null,"body":"After I wrote Inductive pal. I tried to check it with the given test:\r\n   Example test_pal_1: pal [0; 1; 0].\r\n   Proof. reflexivity . Qed.\r\n\r\nBut then I get an error:\r\n   Error:\r\n   Tactic failure: The relation pal is not a declared reflexive relation. Maybe you need to require the Setoid     library.\r\n\r\nWhy does it happen? How do I check it if it is not reflexive?"},"comment":{"url":"https://api.github.com/repos/snu-sf-class/pl2016/issues/comments/209320829","html_url":"https://github.com/snu-sf-class/pl2016/issues/60#issuecomment-209320829","issue_url":"https://api.github.com/repos/snu-sf-class/pl2016/issues/60","id":209320829,"user":{"login":"k32l","id":7943961,"avatar_url":"https://avatars.githubusercontent.com/u/7943961?v=3","gravatar_id":"","url":"https://api.github.com/users/k32l","html_url":"https://github.com/k32l","followers_url":"https://api.github.com/users/k32l/followers","following_url":"https://api.github.com/users/k32l/following{/other_user}","gists_url":"https://api.github.com/users/k32l/gists{/gist_id}","starred_url":"https://api.github.com/users/k32l/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/k32l/subscriptions","organizations_url":"https://api.github.com/users/k32l/orgs","repos_url":"https://api.github.com/users/k32l/repos","events_url":"https://api.github.com/users/k32l/events{/privacy}","received_events_url":"https://api.github.com/users/k32l/received_events","type":"User","site_admin":false},"created_at":"2016-04-13T09:06:19Z","updated_at":"2016-04-13T09:06:19Z","body":"When I use constructor, another error appears:\r\nError: No applicable tactic."}}