From 151a6d2e5dd946a857457a575c581ef402dfd772 Mon Sep 17 00:00:00 2001 From: utensil Date: Sun, 2 Jun 2024 19:08:08 +0800 Subject: [PATCH] Start using `\verb<<<|content<<<` --- trees/math-0003.tree | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/trees/math-0003.tree b/trees/math-0003.tree index 6c95a8d..2855064 100644 --- a/trees/math-0003.tree +++ b/trees/math-0003.tree @@ -13,7 +13,7 @@ \p{The following code is taken from [pygments](https://github.com/eric-wieser/pygments/blob/9d0a36c34ae06c3e318ccbc4b9b43ab16e395e35/tests/examplefiles/lean4/Test.lean) to test Lean 4 code highlighting, with only wrapped strings removed because it confuses forester.} -\codeblock{lean}{ +\codeblock{lean}{\verb<<<| /- Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -256,6 +256,11 @@ variable {ι A B : Type*} (𝒜 : ι → A) (ℬ : ι → B) #check 1.0 + 2. + 0.3e1 +#check "\ + This is\na \ + wrapped string." + @[to_additive "See note [foo]"] lemma mul_one : sorry := sorry -} \ No newline at end of file + +<<<} \ No newline at end of file