hahalol (Mar 21 2023 at 12:40): hahalol (Mar 21 2023 at 12:40):(1) no support for nonlinear patterns therefore cannot do dependent types with shared indices
Definition addnn := [n ] |- n ++ n ==> n.
Rewrite Rule addnn.
Variable #1 already taken for hole 1 but used here for hole 2.
(2) and doesnt even compile unless kernel/cClosure.ml is changed from _ to fconstr * stack
and knr_ret : type a. _ -> _ -> pat_state: (fconstr, stack, a) depth -> ?failed: _ -> fconstr * stack -> a =
(3) and could anyone ping @yannl35133 to kinda haste a lil bit on this VIP feature, as there had been no updates to this repo during over two months except for hes new TYPES branch... lol kthxbye
Gaëtan Gilbert (Mar 21 2023 at 12:50):3) you're not his boss so relax your expectations a bit
also you're looking at the wrong place if you can't see recent updates
Théo Winterhalter (Mar 21 2023 at 13:50):Yes, please don't pressure people that have made absolutely no promise to you. It is anyway unreasonable to ask him to "haste a lil bit". If you want to provide feedback you are welcome to do so, but please do it respectfully to other people's work.
And yes there is no support for nonlinear patterns but that is not a bug, it's just not a feature. There is some leeway in that you can write
Definition addnn := [ n (m := n) ] |- n ++ m ==> n.
where the definition m := n is used for tying but ignored for reduction.
Yann Leray (Mar 21 2023 at 14:15):(1) Can you provide a MetaCoq development or at least a paper which both formalises non-linearity in rewrite rules in Coq and proves calculus properties like confluence and subject reduction with them ? I write this extension along with a MetaCoq proof that it works reasonably well, I won't get ahead of it that much
(2) Just upgrade your OCaml compiler
(3) That would be me. You can ping me, but expect answers as nice as your post
Emilio Jesús Gallego Arias (Mar 22 2023 at 17:15):In addition to what is has been said, an account named "hahalol" is borderline wrt to our community guidelines / CoC, as in particular, while we don't require real names here, that kind of trolling-purposed accounts won't be allowed.
So consider this strike one, more trolling and I will propose a ban.
Last updated: Oct 13 2024 at 01:02 UTC