Skip to content

Commit 5e5e984

Browse files
committed
Prop: simnplify Data.Sum import
1 parent 584d3a9 commit 5e5e984

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/Vatras/Data/Prop/Properties.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ import Data.Bool as Bool
44
open import Data.Bool.Properties using (∧-comm; ∧-zeroˡ; ∧-zeroʳ)
55
open import Data.Empty using (⊥)
66
open import Data.Product as Product using (Σ; _×_; ∃-syntax; _,_)
7-
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
7+
open import Data.Sum using (_⊎_; inj₁; inj₂)
88

99
open import Relation.Nullary.Negation renaming (¬_ to negate)
1010
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong; sym; trans)

0 commit comments

Comments
 (0)