From 8bc705c0abbd506748e2ef5ba8139a3a6b7d3497 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 24 Jun 2024 11:34:14 -0500 Subject: [PATCH] lol --- .vscode/settings.json | 5 ++++- src/CubicalHott/Chapter1.lagda.md | 2 +- src/CubicalHott/Chapter2.lagda.md | 2 +- src/CubicalHott/Chapter2Lemma221.lagda.md | 2 +- src/CubicalHott/Chapter3.lagda.md | 2 +- src/CubicalHott/Chapter6.lagda.md | 2 +- src/CubicalHott/Primitives.agda | 2 +- src/CubicalHott/Primitives/Interval.lagda.md | 2 +- src/CubicalHott/Primitives/Kan.lagda.md | 2 +- src/CubicalHott/Primitives/Type.lagda.md | 2 +- 10 files changed, 13 insertions(+), 10 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index ae378ca..96ece24 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -3,5 +3,8 @@ "gitdoc.enabled": false, "gitdoc.autoCommitDelay": 300000, "gitdoc.commitMessageFormat": "'auto gitdoc commit'", - "agdaMode.connection.commandLineOptions": "" + "agdaMode.connection.commandLineOptions": "", + "search.exclude": { + "src/HottBook/**": true + } } diff --git a/src/CubicalHott/Chapter1.lagda.md b/src/CubicalHott/Chapter1.lagda.md index 97797df..afec5ac 100644 --- a/src/CubicalHott/Chapter1.lagda.md +++ b/src/CubicalHott/Chapter1.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Chapter1 where open import CubicalHott.Primitives public diff --git a/src/CubicalHott/Chapter2.lagda.md b/src/CubicalHott/Chapter2.lagda.md index 1fca2d5..ae42b9b 100644 --- a/src/CubicalHott/Chapter2.lagda.md +++ b/src/CubicalHott/Chapter2.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Chapter2 where open import CubicalHott.Chapter1 diff --git a/src/CubicalHott/Chapter2Lemma221.lagda.md b/src/CubicalHott/Chapter2Lemma221.lagda.md index 097be26..279e053 100644 --- a/src/CubicalHott/Chapter2Lemma221.lagda.md +++ b/src/CubicalHott/Chapter2Lemma221.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Chapter2Lemma221 where open import CubicalHott.Chapter1 diff --git a/src/CubicalHott/Chapter3.lagda.md b/src/CubicalHott/Chapter3.lagda.md index b0073ef..91c6441 100644 --- a/src/CubicalHott/Chapter3.lagda.md +++ b/src/CubicalHott/Chapter3.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Chapter3 where open import CubicalHott.Chapter1 diff --git a/src/CubicalHott/Chapter6.lagda.md b/src/CubicalHott/Chapter6.lagda.md index 3025b3b..09959ff 100644 --- a/src/CubicalHott/Chapter6.lagda.md +++ b/src/CubicalHott/Chapter6.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Chapter6 where open import CubicalHott.Chapter1 diff --git a/src/CubicalHott/Primitives.agda b/src/CubicalHott/Primitives.agda index 7de7b90..8898faa 100644 --- a/src/CubicalHott/Primitives.agda +++ b/src/CubicalHott/Primitives.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Primitives where open import CubicalHott.Primitives.Interval public diff --git a/src/CubicalHott/Primitives/Interval.lagda.md b/src/CubicalHott/Primitives/Interval.lagda.md index a71543f..bc29ffa 100644 --- a/src/CubicalHott/Primitives/Interval.lagda.md +++ b/src/CubicalHott/Primitives/Interval.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Primitives.Interval where open import CubicalHott.Primitives.Type diff --git a/src/CubicalHott/Primitives/Kan.lagda.md b/src/CubicalHott/Primitives/Kan.lagda.md index 7e4419c..dcaf63b 100644 --- a/src/CubicalHott/Primitives/Kan.lagda.md +++ b/src/CubicalHott/Primitives/Kan.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Primitives.Kan where open import CubicalHott.Primitives.Type diff --git a/src/CubicalHott/Primitives/Type.lagda.md b/src/CubicalHott/Primitives/Type.lagda.md index a1a87dd..b56e305 100644 --- a/src/CubicalHott/Primitives/Type.lagda.md +++ b/src/CubicalHott/Primitives/Type.lagda.md @@ -1,5 +1,5 @@ ``` -{-# OPTIONS --cubical #-} +{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Primitives.Type where ```