{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/427","labels_url":"https://api.github.com/repos/leanprover/lean/issues/427/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/427/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/427/events","html_url":"https://github.com/leanprover/lean/issues/427","id":57374257,"number":427,"title":"contexts and universe (variable) parameters","user":{"login":"javra","id":148927,"avatar_url":"https://avatars.githubusercontent.com/u/148927?v=3","gravatar_id":"","url":"https://api.github.com/users/javra","html_url":"https://github.com/javra","followers_url":"https://api.github.com/users/javra/followers","following_url":"https://api.github.com/users/javra/following{/other_user}","gists_url":"https://api.github.com/users/javra/gists{/gist_id}","starred_url":"https://api.github.com/users/javra/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/javra/subscriptions","organizations_url":"https://api.github.com/users/javra/orgs","repos_url":"https://api.github.com/users/javra/repos","events_url":"https://api.github.com/users/javra/events{/privacy}","received_events_url":"https://api.github.com/users/javra/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":5,"created_at":"2015-02-11T20:42:32Z","updated_at":"2015-02-12T00:29:04Z","closed_at":"2015-02-11T23:52:47Z","body":"in the following example, the last three checks shouldn't work and the output of the first two checks should be different.\r\n```\r\nimport algebra.groupoid\r\n\r\nopen precategory truncation eq nat\r\nopen equiv groupoid morphism sigma sigma.ops prod\r\nopen path_algebra\r\n\r\nnamespace gamma\r\n  context\r\n  universe l\r\n  parameters {D₀ : Type.{l}}\r\n    [D₀set : is_hset D₀]\r\n    [C : groupoid.{l l} D₀]\r\n    (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d),\r\n      Type.{l})\r\n  include D₀set C\r\n\r\n  protected definition gamma_CM2_gadget ⦃x : D₀⦄ (a lidu : hom x x)\r\n    (v : D₂ a id id id) (u : D₂ lidu id id id) :=\r\n  u\r\n\r\n  set_option pp.universes true\r\n  check gamma_CM2_gadget.{l}\r\n  check gamma_CM2_gadget.{l l}\r\n  check C.{l}\r\n  check C.{l l}\r\n  check C.{3}\r\n\r\n  end\r\nend gamma\r\n```"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/73994952","html_url":"https://github.com/leanprover/lean/issues/427#issuecomment-73994952","issue_url":"https://api.github.com/repos/leanprover/lean/issues/427","id":73994952,"user":{"login":"leodemoura","id":2778936,"avatar_url":"https://avatars.githubusercontent.com/u/2778936?v=3","gravatar_id":"","url":"https://api.github.com/users/leodemoura","html_url":"https://github.com/leodemoura","followers_url":"https://api.github.com/users/leodemoura/followers","following_url":"https://api.github.com/users/leodemoura/following{/other_user}","gists_url":"https://api.github.com/users/leodemoura/gists{/gist_id}","starred_url":"https://api.github.com/users/leodemoura/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leodemoura/subscriptions","organizations_url":"https://api.github.com/users/leodemoura/orgs","repos_url":"https://api.github.com/users/leodemoura/repos","events_url":"https://api.github.com/users/leodemoura/events{/privacy}","received_events_url":"https://api.github.com/users/leodemoura/received_events","type":"User","site_admin":false},"created_at":"2015-02-12T00:29:04Z","updated_at":"2015-02-12T00:29:04Z","body":"> Yes I'd strongly prefer to reject such terms if @avigad or @fpvandoorn find this confusing as well.\r\n\r\nGreat. \r\nBTW, I just tried it, and no library file is affected by this change.\r\n"}}