From 45d193f649a5e892072dccd2f627154045955d51 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 20 Mar 2024 15:45:59 +0100
Subject: [PATCH] Update gitignore and make agda code compilable

---
 .gitignore            | 2 ++
 agda/algebra.lagda.md | 1 +
 2 files changed, 3 insertions(+)

diff --git a/.gitignore b/.gitignore
index f105203..d53be04 100644
--- a/.gitignore
+++ b/.gitignore
@@ -306,3 +306,5 @@ TSWLatexianTemp*
 MAlonzo/**
 
 *.html
+agda/public
+agda/Everything.agda
diff --git a/agda/algebra.lagda.md b/agda/algebra.lagda.md
index 63afea7..7b75ae7 100644
--- a/agda/algebra.lagda.md
+++ b/agda/algebra.lagda.md
@@ -1,4 +1,5 @@
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import equality
 module algebra where
 ```