coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Pierre Courtieu <pierre.courtieu AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?
Date: Fri, 3 Apr 2020 16:52:49 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f170.google.com
Ironport-phdr: 9a23:u9pNVBT0wCdXVfQeMt4dtJixddpsv+yvbD5Q0YIujvd0So/mwa6zZhGN2/xhgRfzUJnB7Loc0qyK6v2mATJLuM3R+DBaKdoQDkND0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/2O+94YDcbBtVjzShf7xyMA+2rQLMvcUKnIduMKk8xgbJr3dSZ+hbxGxkKU+dkhv/+8y8+IJv/zlKt/8u6sJNXr/2c7gkQbBdET8rL3076Mr3uBbMSgeC+mESWXgMnBpSBAjF4hD6XpPvvSb/q+FwxiqUM9DoQL4tQTit4LtlRxHuiCccKj4263rXhdBqjKJaux2uuRpyyJPJbY6PNfp+eqTdfc4GRWdEQ81cWTBNDp+6YoASFOcKI/pWoJfhqFsPtRu+BBejBOXzyj9Tm3T62bQ23/k9HQ3a2QAtGc8FvnbJo9XvLKocX+C7wrfVwzvAbfxW1zDz54fUfR4uuvyMQbB9fNDNxUQ1Cw/JkFOdopHlMTOP0eQNtnCW4+RiVeKojW4nqgJxrSarxsgylIbEnY0VylXe+iV4xIY5P8G3SEl+YdKqDZBdsCOaN4xwQsMjQGFnpiI6xaMYtpOgcygKzY4oxx/ba/Cdb4eI5RfjWf+XLDxlh3xlYKqyiwiu/UWk0OHxVcm53ExUoiZbjNXArG0B2h7P5sSfVPdw/1ut1SuK2gzO7uxLPUU5mKXaJpI93rI9k4cfvEreESLzhEr7g7GZe0ch9+Wo7+nnbLvmq5qSN4BqlA3zNqEjlde7DOslLwcDWXWQ9/6m273550L5Ra1Hjv0onandt5DXPcEbqbS4Aw9Ry4oj8hW/Ayq/3NQWgHUKLk5JdAiIj4juPFHOL/T4Aumlj1uwlzdrwujKPrznAprTMnjOiKntcap55kJGywc+zcpT64xKBr0fOv7/R038uMDAAh88KQO0wuLnCNtn1oMZXGKCGq2ZMKTUsV+J5eIgPe2Ma5ELtzvmJPgl4uThjX49mVMHYaap2p4XZGiiHvt6O0WZfWbsgtAZHGgWuQo+VfXmh0GGUT5OfHm/RLk85zE+CIK+F4jPXIGtgLqb3Ce6BJJafG5GCkrfWUvvIr2FVu0WZWq5JdJ7jj0JSPD1U44szwuj8gT91qB7L+fJ0iIdvJPnktNy4ruAuws18Gk+DcOb0mKAS2x5tmwNTj4ymqt4pAY1nlWE16l7jvhVGPRc4vpIVkExMpuKnL8yMMz7Rg+UJoTBc12hWNjzRGhpFotske9LWF50HpCZtj6G3yeuBOVLxbmCBZhx66GFmnaoeJ47xHHB260syVIhR5kXbDz0tutE7wHWQrXxvQCcnqeue74b2XeUpmiGxGuK+kpfVVwpCPmXbTUkfkLT6O/ByAbaVbb3UOYoNwJAzYiJLa4YMtA=

On Thu, 2 Apr 2020 22:29:57 +0200
Pierre Courtieu
<pierre.courtieu AT gmail.com>
wrote:

> Hi Jonathan
> Nice!
> P

Thanks! BTW - when I wrote "idempotent" about minlines in my last email, I
meant order preserving.

With move_up_types, would it make sense to move non-Props above Props
only when the consequent is a Prop, and vice versa otherwise? Maybe it
has to do with the domain you're working in. With pure math, I guess
one would see mostly Prop consequents. With software, I guess one
would see many more non-Prop consequents.

[Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/01/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Samuel Gruetter, 04/02/2020
  - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
    - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
      - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
        
        Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/02/2020
        
        Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Pierre Courtieu, 04/02/2020
        
        Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, jonikelee AT gmail.com, 04/03/2020
- Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Paolo Giarrusso, 04/09/2020
  - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Agnishom Chattopadhyay, 04/10/2020
    - Re: [Coq-Club] Fwd: Hiding "Obvious" Hypothesis?, Paolo Giarrusso, 04/10/2020