coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Alternative to Set Hyps Limit
- Date: Sat, 07 Jun 2014 12:17:15 -0400
When dealing with goals having more hypotheses than can fit on the screen at once, is there an alternative to Set Hyps Limit that tries not to hide "useful" hypotheses? I know that "useful" is a very subject term here, but just about any interpretation would be helpful. Otherwise, I have the following proposal: If there is a set of hypotheses in a goal of exactly the same type, have a mode where they are all placed on the same line (subject to line length setting restrictions). For example, a goal like:
a : T
b : T
c : T
d : T
...
====
foo a b c d ...
would get displayed instead as:
a b c d : T
...
====
foo a b c d ...
as long as all of those T's are really the same type (i.e.: not different due to implicit args).
-- Jonathan
- [Coq-Club] Alternative to Set Hyps Limit, Jonathan, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Pierre-Marie Pédrot, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Jonathan, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Abhishek Anand, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Jonathan, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Pierre Courtieu, 06/09/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Jonathan, 06/07/2014
- Re: [Coq-Club] Alternative to Set Hyps Limit, Pierre-Marie Pédrot, 06/07/2014
Archive powered by MHonArc 2.6.18.