diff --git a/.github/ISSUE_TEMPLATE/NoteDocString.yml b/.github/ISSUE_TEMPLATE/NoteDocString.yml new file mode 100644 index 00000000..c97bcbab --- /dev/null +++ b/.github/ISSUE_TEMPLATE/NoteDocString.yml @@ -0,0 +1,24 @@ +name: Note doc string +description: Improvements to docstrings from curated notes +title: "[doc-string]: " +body: + - type: markdown + attributes: + value: | + Thanks for taking the time to suggest an improvement! + - type: input + id: name + attributes: + label: Name of result + description: What is the name of the result you are suggesting an improvement for? + placeholder: + validations: + required: true + - type: textarea + id: improvement + attributes: + label: Improvement + description: What is the improvement you are suggesting? + placeholder: + validations: + required: true diff --git a/docs/CuratedNotes/HarmonicOscillator.html b/docs/CuratedNotes/HarmonicOscillator.html index 27db4fd4..d599894a 100644 --- a/docs/CuratedNotes/HarmonicOscillator.html +++ b/docs/CuratedNotes/HarmonicOscillator.html @@ -1,105 +1,4 @@ --- -layout: default +layout: curatedNote +data_source: harmonicOscillator --- - - - - - - - - -
- - Toggle background color - -
- -

{{ site.data.harmonicOscillator.title }}

-

Note Authors: {{ site.data.harmonicOscillator.curators }}

- - -
-
-

- These notes are created using an interactive theorem - prover called Lean. - Lean formally checks definitions, theorems and proofs for correctness. - These notes are part of a much larger project called - PhysLean, which aims to digitalize - physics into Lean. Please consider contributing to this project. -

- Please provide feedback or suggestions for improvements by creating a GitHub issue - here. -

-
- -
-

Table of content

-

-{% for entry in site.data.harmonicOscillator.parts %} -{% if entry.type == "h1" %} - {{ entry.sectionNo }}. {{ entry.content }}
-{% endif %} -{% if entry.type == "h2" %} -    {{ entry.sectionNo }}. {{ entry.content }}
-{% endif %} -{% endfor %} -

-
- -
-{% for entry in site.data.harmonicOscillator.parts %} - {% if entry.type == "h1" %} -

{{ entry.sectionNo }}. {{ entry.content }}

- {% endif %} - {% if entry.type == "h2" %} -

{{ entry.sectionNo }}. {{ entry.content }}

- {% endif %} - {% if entry.type == "p" %} -

{{ entry.content }}

- {% endif %} - {% if entry.type == "warning" %} - - {% endif %} - {% if entry.type == "name" %} - -
- - - {% if entry.isDef %}Definition{% else %} - {% if entry.isThm %}Theorem{% else %}Lemma{% endif %}{% endif %} {{ entry.declNo }} - ({{ entry.name }}): - {% if entry.status == "incomplete" %}🚧{% endif %} -
{{ entry.docString | markdownify}}
-
- Show Lean code: -
{{ entry.declString }}
-
-
- {% endif %} - {% if entry.type == "remark" %} -
- Remark: {{ entry.name}} - {{ entry.content|markdownify }} -
-
- {% endif %} -{% endfor %} diff --git a/docs/CuratedNotes/HiggsPotential.html b/docs/CuratedNotes/HiggsPotential.html new file mode 100644 index 00000000..43e97a07 --- /dev/null +++ b/docs/CuratedNotes/HiggsPotential.html @@ -0,0 +1,4 @@ +--- +layout: curatedNote +data_source: higgsPotential +--- diff --git a/docs/CuratedNotes/WickTheorem.html b/docs/CuratedNotes/WickTheorem.html new file mode 100644 index 00000000..00b6c29e --- /dev/null +++ b/docs/CuratedNotes/WickTheorem.html @@ -0,0 +1,4 @@ +--- +layout: curatedNote +data_source: perturbationTheory +--- diff --git a/docs/CuratedNotes/index.html b/docs/CuratedNotes/index.html index 0cac1384..a5999686 100644 --- a/docs/CuratedNotes/index.html +++ b/docs/CuratedNotes/index.html @@ -4,17 +4,27 @@

Curated Notes

+

Quantum Harmonic Oscillator

The formalization of the quantum harmonic oscillator.

Read More →
+ +
-

Proof of Wick's theorem

- +

Wick's theorem

The formalization of the proof of Wick's theorem in perturbation theory.

- Read More → + Read More → +
+ + +
+

Higgs potential 🚧

+

The formalization of properties of the Higgs potential.

+ Read More →
+
diff --git a/docs/CuratedNotes/PerturbationTheory.html b/docs/_layouts/curatedNote.html similarity index 86% rename from docs/CuratedNotes/PerturbationTheory.html rename to docs/_layouts/curatedNote.html index 847da763..95abf8b9 100644 --- a/docs/CuratedNotes/PerturbationTheory.html +++ b/docs/_layouts/curatedNote.html @@ -1,6 +1,9 @@ --- layout: default +data_source: harmonicOscillator # Default value, can be overridden --- + +