Skip to content

Commit a5fc597

Browse files
committed
Prop: rename "never" to "negate"
1 parent b8862b8 commit a5fc597

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

src/Vatras/Data/Prop/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ open import Data.Empty using (⊥)
66
open import Data.Product as Product using (Σ; _×_; ∃-syntax; _,_)
77
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
88

9-
open import Relation.Nullary.Negation renaming (¬_ to never)
9+
open import Relation.Nullary.Negation renaming (¬_ to negate)
1010
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong; sym; trans)
1111
open Eq.≡-Reasoning
1212

@@ -68,7 +68,7 @@ Nonconst : Prop F → Set
6868
Nonconst p = Satisfiable p × Falsifiable p
6969

7070
Nonconst' : Prop F Set
71-
Nonconst' p = never (Const p)
71+
Nonconst' p = negate (Const p)
7272

7373
Nonconst→Nonconst' : {p} Nonconst p Nonconst' p
7474
Nonconst→Nonconst' {p} (_ , (a , a-makes-false)) (inj₁ taut ) = NonContradiction' p a (taut a) a-makes-false

0 commit comments

Comments
 (0)