{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/331","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/331/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/331/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/331/events","html_url":"https://github.com/FStarLang/FStar/issues/331","id":102759112,"number":331,"title":"Refinements on mutually recursive sum types","user":{"login":"jkzinzindohoue","id":9868015,"avatar_url":"https://avatars.githubusercontent.com/u/9868015?v=3","gravatar_id":"","url":"https://api.github.com/users/jkzinzindohoue","html_url":"https://github.com/jkzinzindohoue","followers_url":"https://api.github.com/users/jkzinzindohoue/followers","following_url":"https://api.github.com/users/jkzinzindohoue/following{/other_user}","gists_url":"https://api.github.com/users/jkzinzindohoue/gists{/gist_id}","starred_url":"https://api.github.com/users/jkzinzindohoue/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jkzinzindohoue/subscriptions","organizations_url":"https://api.github.com/users/jkzinzindohoue/orgs","repos_url":"https://api.github.com/users/jkzinzindohoue/repos","events_url":"https://api.github.com/users/jkzinzindohoue/events{/privacy}","received_events_url":"https://api.github.com/users/jkzinzindohoue/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/FStarLang/FStar/labels/question","name":"question","color":"cc317c"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":5,"created_at":"2015-08-24T10:22:04Z","updated_at":"2015-08-27T09:45:30Z","closed_at":null,"body":"I would like to write something like to following : \r\n\r\n```fsharp\r\ntype list1 (a:Type) =\r\n  | Nil1 : list1 a\r\n  | Cons1: hd:a -> tl:list2 a -> list1 a\r\nand list2 (a:Type) =\r\n  | List: t:uint8{t=0uy \\/ t=1uy} -> \r\n           v:list a{ (t=0uy <==> is_Nil1 v)\r\n                     /\\ (t=1uy <==> is_Cons1 v) } ->\r\n           list2 a\r\n```\r\n\r\nHowever the identifiers `is_Nil1` and `is_Cons1` are unknown to F* at this point. Is it possible to make F* aware of those constructors ?\r\nIs there another way to write that ?"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/135366869","html_url":"https://github.com/FStarLang/FStar/issues/331#issuecomment-135366869","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/331","id":135366869,"user":{"login":"s-zanella","id":7451757,"avatar_url":"https://avatars.githubusercontent.com/u/7451757?v=3","gravatar_id":"","url":"https://api.github.com/users/s-zanella","html_url":"https://github.com/s-zanella","followers_url":"https://api.github.com/users/s-zanella/followers","following_url":"https://api.github.com/users/s-zanella/following{/other_user}","gists_url":"https://api.github.com/users/s-zanella/gists{/gist_id}","starred_url":"https://api.github.com/users/s-zanella/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/s-zanella/subscriptions","organizations_url":"https://api.github.com/users/s-zanella/orgs","repos_url":"https://api.github.com/users/s-zanella/repos","events_url":"https://api.github.com/users/s-zanella/events{/privacy}","received_events_url":"https://api.github.com/users/s-zanella/received_events","type":"User","site_admin":false},"created_at":"2015-08-27T09:45:30Z","updated_at":"2015-08-27T09:45:30Z","body":"Note that Agda accepts this kind of inductive-inductive definition:\r\n\r\n```Agda\r\nmodule Shady where\r\n\r\nopen import Data.Bool\r\nopen import Data.Product\r\n\r\nmutual\r\n  data List1 (A : Set) : Set where\r\n    nil1  : List1 A\r\n    cons1 : (hd : A) -> (tl : List2 A) -> List1 A\r\n\r\n  data List2 (A : Set) : Set where\r\n    list2 : (t : Bool) -> \r\n            (v : Σ (List1 A) \r\n                   (λ x -> T (if t then is_nil1 x else is_cons1 x))) ->\r\n            List2 A\r\n\r\n  is_nil1 : ∀ {A : Set} -> List1 A -> Bool\r\n  is_nil1 nil1         = true\r\n  is_nil1 (cons1 _ _)  = false\r\n\r\n  is_cons1 : ∀ {A : Set} -> List1 A -> Bool\r\n  is_cons1 nil1        = false\r\n  is_cons1 (cons1 _ _) = true\r\n```\r\n\r\nNow I'm not saying that the theory behind this is entirely clear, but the idiom is useful enough to raise the question of whether you want F* to support it. Coq is quite conservative in this regard...and Agda is, well, on the opposite end."}}