add nix files to git ignore, update imports in tutorials

agda · Jun 9, 2024 · 2d63a66 · 2d63a66
1 parent 9388b77
commit 2d63a66
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 1 deletion.
diff --git a/.gitignore b/.gitignore
@@ -7,3 +7,7 @@ docs/build/
 *.hi
 *.o
 
+# For nix users
+.direnv/**
+.envrc
+result
diff --git a/tutorials/example-proofs/Ascending.agda b/tutorials/example-proofs/Ascending.agda
@@ -1,7 +1,9 @@
 module Ascending where
 
 open import Haskell.Prelude
-open import Haskell.Prim 
+open import Haskell.Prim
+open import Haskell.Law.Equality using (sym; begin_; _≡⟨⟩_; step-≡; _∎)
+open import Haskell.Law.Bool using (ifTrueEqThen)
 
 -- function judging ascending order on lists
 isAscending : ⦃ iOrdA : Ord a ⦄ → List a → Bool

diff --git a/tutorials/example-proofs/Triangle.agda b/tutorials/example-proofs/Triangle.agda
@@ -1,6 +1,7 @@
 module Triangle where
 
 open import Haskell.Prelude
+open import Haskell.Law.Bool using (&&-rightTrue; &&-leftTrue)
 
 -- helper function
 countBiggerThan : ⦃ Ord a ⦄ → List a → a → Int
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,3 +7,7 @@ docs/build/ @@
     *.hi
     *.o
+    # For nix users
+    .direnv/**
+    .envrc
+    result