Skip to content

Commit

Permalink
chore(100,1000.html): remove mention of formalised statements (#579)
Browse files Browse the repository at this point in the history
The previous PR broke the webpage build; I don't understand why.
Hopefully, reverting this fixes it.
  • Loading branch information
grunweg authored Jan 20, 2025
1 parent 5a01e7c commit 5cadbea
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 26 deletions.
13 changes: 0 additions & 13 deletions templates/100-missing.html
Original file line number Diff line number Diff line change
Expand Up @@ -11,18 +11,5 @@
* {{ theorem.id }}: {{ theorem.title }}
{% endfor %}

The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome.
{% for theorem in thousand_theorems|selectattr('statement_formalized') %}
<h5 class="markdown-heading mt-5" id="{{ theorem.id }}">{{ theorem.id }}: {{ theorem.title }} <a class="hover-link" href="#{{ theorem.id }}">#</a></h5>
{% if theorem.authors %}<p>Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}</p>{% endif %}
{% if theorem.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}
{% for doc in theorem.doc_decls|default([], true) %}
<div class="doc-stmt">{{ doc.decl_header_html }}</div>
<p><a href="{{ doc.docs_link }}">docs</a>, <a href="{{ doc.src_link }}">source</a></p>
{% endfor %}
{% for title, link in (theorem.links|default({}, true)).items() %}<p><a href="{{link}}">{{title}}</a></p>{% endfor %}
{% if theorem.note %}<p>{% markdown %}{{ theorem.note }}{% endmarkdown %}</p>{% endif %}
{% endfor %}

{% endmarkdown %}
{% endblock %}
13 changes: 0 additions & 13 deletions templates/1000-missing.html
Original file line number Diff line number Diff line change
Expand Up @@ -11,18 +11,5 @@
* {{ theorem.id }}: {{ theorem.title }}
{% endfor %}

The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome.
{% for theorem in thousand_theorems|selectattr('statement_formalized') %}
<h5 class="markdown-heading mt-5" id="{{ theorem.id }}">{{ theorem.id }}: {{ theorem.title }} <a class="hover-link" href="#{{ theorem.id }}">#</a></h5>
{% if theorem.authors %}<p>Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}</p>{% endif %}
{% if theorem.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}
{% for doc in theorem.doc_decls|default([], true) %}
<div class="doc-stmt">{{ doc.decl_header_html }}</div>
<p><a href="{{ doc.docs_link }}">docs</a>, <a href="{{ doc.src_link }}">source</a></p>
{% endfor %}
{% for title, link in (theorem.links|default({}, true)).items() %}<p><a href="{{link}}">{{title}}</a></p>{% endfor %}
{% if theorem.note %}<p>{% markdown %}{{ theorem.note }}{% endmarkdown %}</p>{% endif %}
{% endfor %}

{% endmarkdown %}
{% endblock %}

0 comments on commit 5cadbea

Please sign in to comment.