Update gitignore and make agda code compilable
This commit is contained in:
parent
98c38160ff
commit
45d193f649
2 changed files with 3 additions and 0 deletions
2
.gitignore
vendored
2
.gitignore
vendored
|
@ -306,3 +306,5 @@ TSWLatexianTemp*
|
||||||
MAlonzo/**
|
MAlonzo/**
|
||||||
|
|
||||||
*.html
|
*.html
|
||||||
|
agda/public
|
||||||
|
agda/Everything.agda
|
||||||
|
|
|
@ -1,4 +1,5 @@
|
||||||
```agda
|
```agda
|
||||||
|
{-# OPTIONS --allow-unsolved-metas #-}
|
||||||
open import equality
|
open import equality
|
||||||
module algebra where
|
module algebra where
|
||||||
```
|
```
|
||||||
|
|
Loading…
Reference in a new issue