Beter formatting for proofs (thmproof, qedhere)

README.md

@@ -34,7 +34,7 @@ The [differential_calculus.typ](differential_calculus.typ) ([render](differentia
 ### Preamble
 ```typst
 #import "theorems.typ": *
-#show: thmrules
+#show: thmrules.with(qed-symbol: $square$)
 
 #set page(width: 16cm, height: auto, margin: 1.5cm)
 #set text(font: "Linux Libertine", lang: "en")
@@ -50,12 +50,7 @@ The [differential_calculus.typ](differential_calculus.typ) ([render](differentia
 #let definition = thmbox("definition", "Definition", inset: (x: 1.2em, top: 1em))
 
 #let example = thmplain("example", "Example").with(numbering: none)
-#let proof = thmplain(
-  "proof",
-  "Proof",
-  base: "theorem",
-  bodyfmt: body => [#body #h(1fr) $square$]
-).with(numbering: none)
+#let proof = thmproof("proof", "Proof")
 ```
 
 ### Document
@@ -88,6 +83,15 @@ The [differential_calculus.typ](differential_calculus.typ) ([render](differentia
 #corollary[
   There are infinitely many composite numbers.
 ]
+
+#theorem[
+  There are arbitrarily long stretches of composite numbers.
+]
+#proof[
+  For any $n > 2$, consider $
+    n! + 2, quad n! + 3, quad ..., quad n! + n #qedhere
+  $
+]
 ```
 
 

basic.typ

@@ -1,5 +1,5 @@
 #import "theorems.typ": *
-#show: thmrules
+#show: thmrules.with(qed-symbol: $square$)
 
 #set page(width: 16cm, height: auto, margin: 1.5cm)
 #set text(font: "Linux Libertine", lang: "en")
@@ -15,12 +15,7 @@
 #let definition = thmbox("definition", "Definition", inset: (x: 1.2em, top: 1em))
 
 #let example = thmplain("example", "Example").with(numbering: none)
-#let proof = thmplain(
-  "proof",
-  "Proof",
-  base: "theorem",
-  bodyfmt: body => [#body #h(1fr) $square$]
-).with(numbering: none)
+#let proof = thmproof("proof", "Proof")
 
 
 = Prime numbers
@@ -51,3 +46,12 @@
 #corollary[
   There are infinitely many composite numbers.
 ]
+
+#theorem[
+  There are arbitrarily long stretches of composite numbers.
+]
+#proof[
+  For any $n > 2$, consider $
+    n! + 2, quad n! + 3, quad ..., quad n! + n #qedhere
+  $
+]

differential_calculus.typ

@@ -42,14 +42,11 @@
 ).with(numbering: none)
 
 // Proofs are attached to theorems, although they are not numbered
-#let proof = thmplain(
+#let proof = thmproof(
   "proof",
   "Proof",
   base: "theorem",
-  bodyfmt: body => [
-    #body #h(1fr) $square$    // Insert QED symbol
-  ]
-).with(numbering: none)
+)
 
 #let solution = thmplain(
   "solution",

manual.typ

@@ -41,8 +41,8 @@ Import all functions provided by `typst-theorems` using
 The second line is crucial for displaying `thmenv`s and references correctly!
 
 The core of this module consists of `thmenv`.
-The functions `thmbox` and `thmplain` provide some simple defaults for the
-appearance of `thmenv`s.
+The functions `thmbox`, `thmplain`, and `thmproof` provide some simple
+defaults for the appearance of `thmenv`s.
 
 
 = Feature demonstration <feat>
@@ -138,6 +138,60 @@ numbering pattern as described in the
 documentation.
 
 
+== Proofs
+
+The `thmproof` function gives nicer defaults for formatting proofs.
+```typst
+#let proof = thmproof("proof", "Proof")
+
+#proof([of @euclid])[
+  Suppose to the contrary that $p_1, p_2, dots, p_n$ is a finite enumeration
+  of all primes. Set $P = p_1 p_2 dots p_n$. Since $P + 1$ is not in our list,
+  it cannot be prime. Thus, some prime factor $p_j$ divides $P + 1$.  Since
+  $p_j$ also divides $P$, it must divide the difference $(P + 1) - P = 1$, a
+  contradiction.
+]
+```
+#let proof = thmproof("proof", "Proof")
+
+#proof([of @euclid])[
+  Suppose to the contrary that $p_1, p_2, dots, p_n$ is a finite enumeration
+  of all primes. Set $P = p_1 p_2 dots p_n$. Since $P + 1$ is not in our list,
+  it cannot be prime. Thus, some prime factor $p_j$ divides $P + 1$.  Since
+  $p_j$ also divides $P$, it must divide the difference $(P + 1) - P = 1$, a
+  contradiction.
+]
+
+If your proof ends in a block equation, or a list/enum, you can place
+`qedhere` to correctly position the qed symbol.
+```typst
+#theorem[
+  There are arbitrarily long stretches of composite numbers.
+]
+#proof[
+  For any $n > 2$, consider $
+    n! + 2, quad n! + 3, quad ..., quad n! + n #qedhere
+  $
+]
+```
+#theorem[
+  There are arbitrarily long stretches of composite numbers.
+]
+#proof[
+  For any $n > 2$, consider $
+    n! + 2, quad n! + 3, quad ..., quad n! + n #qedhere
+  $
+]
+
+*Caution*: The `qedhere` symbol does not play well with numbered/multiline
+equations!
+
+You can set a custom qed symbol (say $square$) by setting the appropriate
+option in `thmrules` as follows.
+```typst
+#show: thmrules.with(qed-symbol: $square$)
+```
+
 == Suppressing numbering
 Supplying `numbering: none` to an environment suppresses numbering for that
 block, and prevents it from updating its counter.
@@ -252,7 +306,7 @@ The `thmbox` function lets you specify rules for formatting the `title`, the
 and `number` together.
 
 ```typst
-#let proof = thmplain(
+#let proof-custom = thmplain(
   "proof",
   "Proof",
   base: "theorem",
@@ -265,13 +319,13 @@ and `number` together.
 #lemma[
   All even natural numbers greater than 2 are composite.
 ]
-#proof[
+#proof-custom[
   Every even natural number $n$ can be written as the product of the natural
   numbers $2$ and $n\/2$. When $n > 2$, both of these are smaller than $2$
   itself.
 ]
 ```
-#let proof = thmplain(
+#let proof-custom = thmplain(
   "proof",
   "Proof",
   base: "theorem",
@@ -284,7 +338,7 @@ and `number` together.
 #lemma[
   All even natural numbers greater than 2 are composite.
 ]
-#proof[
+#proof-custom[
   Every even natural number $n$ can be written as the product of the natural
   numbers $2$ and $n\/2$. When $n > 2$, both of these are smaller than $2$
   itself.
@@ -515,6 +569,39 @@ defaults.
 ```
 
 
+== `thmproof`, `proof-bodyfmt` and `qedhere`
+
+The `thmproof` function is identical to `thmplain`, except with defaults
+appropriate for proofs.
+
+```typst
+#let thmproof(..args) = thmplain(
+    ..args,
+    namefmt: emph,
+    bodyfmt: proof-bodyfmt,
+).with(numbering: none)
+```
+
+The `proof-bodyfmt` function is a `bodyfmt` function that automatically places
+a qed symbol at the end of the body.
+
+You can place `#qedhere` inside a block equation, or at the end of a list/enum
+item to place the qed symbol on the same line.
+
+
+== `thmrules`
+
+The `thmrules` show rule sets important styling rules for theorem
+environments, references, and equations in proofs.
+
+```typst
+#let thmrules(
+  qed-symbol: $qed$,      // QED symbol used in proofs
+  doc
+) = { ... }
+```
+
+
 = Acknowledgements
 
 Thanks to

manual_examples.typ

@@ -17,6 +17,7 @@
 This document only includes the examples given in the manual; each one of
 these has been explained in full detail there.
 
+
 = Feature demonstration
 
 #let theorem = thmbox(
@@ -29,6 +30,7 @@ these has been explained in full detail there.
   There are infinitely many primes.
 ] <euclid>
 
+
 #let lemma = thmbox(
   "theorem",
   "Lemma",
@@ -51,6 +53,28 @@ these has been explained in full detail there.
 ]
 
 
+== Proofs
+
+#let proof = thmproof("proof", "Proof")
+
+#proof([of @euclid])[
+  Suppose to the contrary that $p_1, p_2, dots, p_n$ is a finite enumeration
+  of all primes. Set $P = p_1 p_2 dots p_n$. Since $P + 1$ is not in our list,
+  it cannot be prime. Thus, some prime factor $p_j$ divides $P + 1$.  Since
+  $p_j$ also divides $P$, it must divide the difference $(P + 1) - P = 1$, a
+  contradiction.
+]
+
+#theorem[
+  There are arbitrarily long stretches of composite numbers.
+]
+#proof[
+  For any $n > 2$, consider $
+    n! + 2, quad n! + 3, quad ..., quad n! + n #qedhere
+  $
+]
+
+
 == Suppressing numbering
 
 #let example = thmplain(
@@ -68,10 +92,12 @@ these has been explained in full detail there.
 #lemma[
   The square of any odd number is one more than a multiple of $4$.
 ]
+
 #lemma(number: "42")[
   The square of any natural number cannot be two more than a multiple of 4.
 ]
 
+
 == Limiting depth
 
 #let definition = thmbox(
@@ -80,7 +106,6 @@ these has been explained in full detail there.
   base_level: 1,
   stroke: rgb("#68ff68") + 1pt
 )
-
 #definition("Prime numbers")[
   A natural number is called a _prime number_ if it is greater than $1$ and
   cannot be written as the product of two smaller natural numbers. <prime>
@@ -98,7 +123,7 @@ these has been explained in full detail there.
 
 == Custom formatting
 
-#let proof = thmplain(
+#let proof-custom = thmplain(
   "proof",
   "Proof",
   base: "theorem",
@@ -111,7 +136,7 @@ these has been explained in full detail there.
 #lemma[
   All even natural numbers greater than 2 are composite.
 ]
-#proof[
+#proof-custom[
   Every even natural number $n$ can be written as the product of the natural
   numbers $2$ and $n\/2$. When $n > 2$, both of these are smaller than $2$
   itself.
@@ -141,6 +166,7 @@ these has been explained in full detail there.
   All multiples of 3 greater than 3 are composite.
 ]
 
+
 == Labels and references <references>
 
 #pad(
@@ -150,6 +176,7 @@ these has been explained in full detail there.
   ]
 )
 
+
 #pad(
   left: 1.2em,
   [
@@ -161,26 +188,19 @@ these has been explained in full detail there.
   All primes apart from $2$ and $3$ are of the form $6k plus.minus 1$.
 ] <primeform>
 
-#pad(
-  left: 1.2em,
-  [
-    You can modify the supplement and numbering to be used in references, like @primeform.
-  ]
-)
+You can modify the supplement and numbering to be used in references, like @primeform.
 
 
 == Overriding `base`
 
-#let remark = thmplain("remark", "Remark", base: "heading")
 
+#let remark = thmplain("remark", "Remark", base: "heading")
 #remark[
   There are infinitely many composite numbers.
 ]
-
 #corollary[
   All primes greater than $2$ are odd.
 ] <oddprime>
-
 #remark(base: "corollary")[
   Two is a _lone prime_.
 ]