From e1e6ebe55257f6884193456edf6acca24d446b03 Mon Sep 17 00:00:00 2001
From: utensil <utensilcandel@gmail.com>
Date: Wed, 13 Dec 2023 23:16:39 +0800
Subject: [PATCH] Add demo in Lean/blueprint and misc fixes

---
 Reconstruction/Test.lean         |  9 ++++++++
 blueprint/src/chapter/intro.tex  | 39 ++++++++++++++++++++++++++++++++
 blueprint/src/preamble/print.tex |  6 +++++
 blueprint/src/print.tex          |  2 +-
 blueprint/src/web.tex            |  2 +-
 5 files changed, 56 insertions(+), 2 deletions(-)

diff --git a/Reconstruction/Test.lean b/Reconstruction/Test.lean
index 0849845..76a78ab 100644
--- a/Reconstruction/Test.lean
+++ b/Reconstruction/Test.lean
@@ -1,3 +1,12 @@
 import Mathlib.Topology.Basic
 
 #check TopologicalSpace
+
+def one := 1
+
+def two := 2
+
+theorem one_plus_one_eq_two : one + one = two := by
+  rfl
+
+def one_plus_one_eq_two_with_def : Prop := one + one = two
diff --git a/blueprint/src/chapter/intro.tex b/blueprint/src/chapter/intro.tex
index e69de29..90d690a 100644
--- a/blueprint/src/chapter/intro.tex
+++ b/blueprint/src/chapter/intro.tex
@@ -0,0 +1,39 @@
+\chapter{Introduction}
+\label{chap:intro}
+
+Formalisation of the proof of the 'germs' version of the reconstruction theorem.
+
+Below are some demos of how to refer to Lean definitions/theorems in the blueprint.
+
+\begin{definition}[One]
+\label{one}
+\lean{one}
+\leanok
+
+    one is 1.
+
+\end{definition}
+
+\begin{definition}[Two]
+\label{two}
+\lean{two}
+\leanok
+
+    two is 2.
+
+\end{definition}
+
+\begin{lemma}[One plus one is two]
+\label{one_plus_one_eq_two}
+\lean{one_plus_one_eq_two}
+\uses{one, two}
+\leanok
+
+one + one = two
+
+\end{lemma}
+
+\begin{proof}
+\leanok
+It is obvious.
+\end{proof}
\ No newline at end of file
diff --git a/blueprint/src/preamble/print.tex b/blueprint/src/preamble/print.tex
index 013b983..6df140b 100644
--- a/blueprint/src/preamble/print.tex
+++ b/blueprint/src/preamble/print.tex
@@ -14,3 +14,9 @@
 \newcommand{\proves}[1]{}
 \newcommand{\lean}[1]{}
 \newcommand{\leanok}{}
+
+% Define `ifplastex` so we can have complicated macros for PDF
+% and simplified macros for the website.
+% See http://plastex.github.io/plastex/plastex/sect0006.html
+\newif\ifplastex
+\plastexfalse
diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex
index e8d57d9..6e8a446 100644
--- a/blueprint/src/print.tex
+++ b/blueprint/src/print.tex
@@ -20,7 +20,7 @@
 \setmathfont[range=\varnothing]{Asana-Math.otf}
 \setmathfont[range=\pitchfork]{Asana-Math.otf}
 \setmathfont[range=\intprod]{Asana-Math.otf}
-\setmathfont[range=\int]{Latin Modern Math}
+\setmathfont[range=\int]{latinmodern-math.otf}
 
 \usepackage[nameinlink, capitalize]{cleveref}
 
diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex
index 447f9ae..f1187d2 100644
--- a/blueprint/src/web.tex
+++ b/blueprint/src/web.tex
@@ -8,7 +8,7 @@
 \usepackage{graphicx}
 \DeclareGraphicsExtensions{.svg,.png,.jpg}
 \usepackage[capitalize]{cleveref}
-\usepackage[showmore, dep_graph, project=../../]{blueprint}
+\usepackage[dep_graph, project=../../]{blueprint}
 
 \usepackage{tikz-cd}
 \usepackage{tikz}