From 60954c21c378c50b6c91239f2a9c18374c11730e Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Wed, 27 Jul 2022 00:28:06 +0200
Subject: [PATCH] fixued issue with definition indecies

---
 src/Parser/Parse.idr | 2 +-
 tests/nat-id.pi      | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr
index de717a5..6d9157f 100644
--- a/src/Parser/Parse.idr
+++ b/src/Parser/Parse.idr
@@ -435,7 +435,7 @@ definitions defs = do
     ty <- expr defs 0 []
     match PTDefEq
     tr <- expr defs 0 []
-    next <- definitions (arg :: defs) <|> pure ([], [])
+    next <- definitions (defs ++ [arg]) <|> pure ([], [])
     pure (arg :: fst next, (ty, tr) :: snd next)
 
 parsePi : List String -> Grammar () PiToken True a -> List (WithBounds PiToken) -> Either String a
diff --git a/tests/nat-id.pi b/tests/nat-id.pi
index 29cd64b..6be9f78 100644
--- a/tests/nat-id.pi
+++ b/tests/nat-id.pi
@@ -1,6 +1,9 @@
 let add : ℕ → ℕ → ℕ
   ≔ ℕ-ind (λ_. ℕ → ℕ) (λn.n) (λn.λan.λm. suc (an m))
 
+let add_test : Id ℕ (add 2 2) 4
+  ≔ refl ℕ 4
+
 let add_id_l : Π (n : ℕ) Id ℕ n (add 0 n)
   ≔ λn. refl ℕ n