Skip to content

Commit 1b13835

Browse files
committed
fixed agda#1930 bug
1 parent 78e11bd commit 1b13835

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

README/Inspect.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Data.Nat.Base
1616
open import Data.Nat.Properties
1717
open import Data.Product.Base using (_×_; _,_)
1818
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
19-
open import Relation.Binary.PropositionalEquality using (inspect)
19+
open import Relation.Binary.PropositionalEquality using (inspect; [_])
2020

2121
------------------------------------------------------------------------
2222
-- Using inspect

0 commit comments

Comments
 (0)