{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/395","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/395/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/395/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/395/events","html_url":"https://github.com/UniMath/UniMath/issues/395","id":163415684,"number":395,"title":"Obligatory use of the existing definitions","user":{"login":"vladimirias","id":424011,"avatar_url":"https://avatars.githubusercontent.com/u/424011?v=3","gravatar_id":"","url":"https://api.github.com/users/vladimirias","html_url":"https://github.com/vladimirias","followers_url":"https://api.github.com/users/vladimirias/followers","following_url":"https://api.github.com/users/vladimirias/following{/other_user}","gists_url":"https://api.github.com/users/vladimirias/gists{/gist_id}","starred_url":"https://api.github.com/users/vladimirias/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vladimirias/subscriptions","organizations_url":"https://api.github.com/users/vladimirias/orgs","repos_url":"https://api.github.com/users/vladimirias/repos","events_url":"https://api.github.com/users/vladimirias/events{/privacy}","received_events_url":"https://api.github.com/users/vladimirias/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":8,"created_at":"2016-07-01T15:08:56Z","updated_at":"2016-07-04T15:21:44Z","closed_at":null,"body":"I suggest the following addition to our rules:\r\n\r\n1. Formalizing a result or a group of results one must use the existing definitions wherever they are available. For example, if the ring of integers appears in the formulation of a theorem or in a definition of a more complex object the existing the definition of [hz] must be used.\r\n\r\nIf a different model of [hz] is more convenient for the proof, including intermediate lemmas, such a definition may be introduced and used as long as a proof of the theorem formulated using the existing definition is also produced. "},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/230313039","html_url":"https://github.com/UniMath/UniMath/issues/395#issuecomment-230313039","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/395","id":230313039,"user":{"login":"vladimirias","id":424011,"avatar_url":"https://avatars.githubusercontent.com/u/424011?v=3","gravatar_id":"","url":"https://api.github.com/users/vladimirias","html_url":"https://github.com/vladimirias","followers_url":"https://api.github.com/users/vladimirias/followers","following_url":"https://api.github.com/users/vladimirias/following{/other_user}","gists_url":"https://api.github.com/users/vladimirias/gists{/gist_id}","starred_url":"https://api.github.com/users/vladimirias/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vladimirias/subscriptions","organizations_url":"https://api.github.com/users/vladimirias/orgs","repos_url":"https://api.github.com/users/vladimirias/repos","events_url":"https://api.github.com/users/vladimirias/events{/privacy}","received_events_url":"https://api.github.com/users/vladimirias/received_events","type":"User","site_admin":false},"created_at":"2016-07-04T15:21:44Z","updated_at":"2016-07-04T15:21:44Z","body":"Then I suggest the following modified version of the rule:\r\n\r\n\"Formalizing a result or a group of results one should use the existing definitions wherever they are available. For example, if the ring of integers appears in the formulation of a theorem or in a definition of a more complex object the existing the definition of [hz] must be used.\r\n\r\nIf, for some reason, a different model of a construction is strongly preferable it must be proved to be equivalent to the existing one.\" "}}
{"actor":{"display_login":"vladimirias"}}