feat: Update website with Curated notes

HEPLean · Feb 27, 2025 · 670859a · 670859a
1 parent 4c9e205
commit 670859a
Show file tree

Hide file tree

Showing 4 changed files with 81 additions and 8 deletions.
diff --git a/PhysLean/Mathematics/List.lean b/PhysLean/Mathematics/List.lean
@@ -49,9 +49,9 @@ lemma takeWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :
     · dsimp only [List.takeWhile]
       simp only [hPa, decide_true, List.eraseIdx_cons_succ, List.cons.injEq, true_and]
       rw [takeWile_eraseIdx]
-      rfl
-      intro i j hij hP
-      simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
+      · rfl
+      · intro i j hij hP
+        simpa using h (Fin.succ i) (Fin.succ j) (by simpa using hij) (by simpa using hP)
     · simp [hPa]
 
 lemma dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] :

diff --git a/docs/CuratedNotes/index.html b/docs/CuratedNotes/index.html
@@ -0,0 +1,72 @@
+---
+layout: default
+---
+<div class="curated-notes">
+  <h1 class="title">Curated Notes</h1>
+  <div class="notes-container">
+    <div class="note-card">
+      <h2 style="text-align: center;">Quantum Harmonic Oscillator</h2>
+      <p class="description">The formalization of the quantum harmonic oscillator.</p>
+      <a href="HarmonicOscillator" class="note-link">Read More →</a>
+    </div>
+    <div class="note-card">
+      <h2 style="text-align: center;">Proof of Wick's theorem</h2>
+
+      <p class="description">The formalization of the proof of Wick's theorem in perturbation theory.</p>
+      <a href="PerturbationTheory" class="note-link">Read More →</a>
+    </div>
+  </div>
+</div>
+
+<style>
+.curated-notes {
+  max-width: 1200px;
+  margin: 2rem auto;
+  padding: 0 1rem;
+}
+
+.title {
+  text-align: center;
+  color: #2c3e50;
+  margin-bottom: 2rem;
+}
+
+.notes-container {
+  display: grid;
+  grid-template-columns: repeat(auto-fit, minmax(300px, 1fr));
+  gap: 2rem;
+}
+
+.note-card {
+  background: #ffffff;
+  border-radius: 8px;
+  padding: 1.5rem;
+  box-shadow: 0 4px 8px rgba(0,0,0,0.2);
+  transition: transform 0.2s ease;
+}
+
+.note-card:hover {
+  transform: translateY(-5px);
+}
+
+.note-card h2 {
+  color: #34495e;
+  margin-bottom: 1rem;
+}
+
+.description {
+  color: #666;
+  margin-bottom: 1.5rem;
+}
+
+.note-link {
+  display: inline-block;
+  color: #2c3e50;
+  text-decoration: none;
+  font-weight: bold;
+}
+
+.note-link:hover {
+  color: #2980b9;
+}
+</style>
diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html
@@ -25,16 +25,17 @@
     <header class="page-header" role="banner">
       <h1 class="project-name">{{ site.title | default: site.github.repository_name }}</h1>
       <h2 class="project-tagline">{{ page.description | default: site.description | default: site.github.project_tagline }}</h2>
-      <a href="./docs/" class="btn">Documentation</a>
+      <a href="/docs/" class="btn">Documentation</a>
+      <a href="/CuratedNotes/index.html" class="btn">Curated notes</a>
       {% if site.github.is_project_page %}
         <a href="{{ site.github.repository_url }}" class="btn">View on GitHub</a>
       {% endif %}
       {% if site.show_downloads %}
         <a href="{{ site.github.zip_url }}" class="btn">Download .zip</a>
         <a href="{{ site.github.tar_url }}" class="btn">Download .tar.gz</a>
       {% endif %}
-      <a href="./TODOList" class="btn">TODO List</a>
-      <a href="./InformalGraph.html" class="btn">Help formalize</a>
+      <a href="/TODOList" class="btn">TODO List</a>
+      <a href="/InformalGraph.html" class="btn">Help formalize</a>
     </header>
 
     <main id="content" class="main-content" role="main">

diff --git a/scripts/Template.lean b/scripts/Template.lean
@@ -60,8 +60,8 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
 
         <header style="background-color: #2C3E50; color: #fff;">
           <h1><label for="nav_toggle"></label><span>
-          <a href="https://heplean.github.io/HepLean/" style="color: #fff; text-decoration: none; font-family: serif">
-          HepLean Documentation</a>
+          <a href="heplean.com" style="color: #fff; text-decoration: none; font-family: serif">
+          PhysLean Documentation</a>
           </span></h1>
           <h2  style="color: #fff; font-family: serif">[breakWithin title]</h2>
           <form action="https://google.com/search" method="get" id="search_form">