Use consistent names for `Decidable` combinators

[jamesmckinna]

agda-stdlib/src/Relation/Nullary/Decidable/Core.agda

Lines 91 to 122 in 2ce5eb3

	------------------------------------------------------------------------
	-- Interaction with negation, sum, product etc.
	infixr 1 _⊎-dec_
	infixr 2 _×-dec_ _→-dec_
	T? : ∀ x → Dec (T x)
	T? x = x because T-reflects x
	¬? : Dec A → Dec (¬ A)
	does (¬? a?) = not (does a?)
	proof (¬? a?) = ¬-reflects (proof a?)
	⊤-dec : Dec {a} ⊤
	does ⊤-dec = true
	proof ⊤-dec = ⊤-reflects
	_×-dec_ : Dec A → Dec B → Dec (A × B)
	does (a? ×-dec b?) = does a? ∧ does b?
	proof (a? ×-dec b?) = proof a? ×-reflects proof b?
	⊥-dec : Dec {a} ⊥
	does ⊥-dec = false
	proof ⊥-dec = ⊥-reflects
	_⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B)
	does (a? ⊎-dec b?) = does a? ∨ does b?
	proof (a? ⊎-dec b?) = proof a? ⊎-reflects proof b?
	_→-dec_ : Dec A → Dec B → Dec (A → B)
	does (a? →-dec b?) = not (does a?) ∨ does b?
	proof (a? →-dec b?) = proof a? →-reflects proof b?

defines

T? : ∀ x → Dec (T x)
¬? : Dec A → Dec (¬ A)
⊤-dec : Dec {a} ⊤
_×-dec_ : Dec A → Dec B → Dec (A × B)
⊥-dec : Dec {a} ⊥
_⊎-dec_ : Dec A → Dec B → Dec (A ⊎ B)
_→-dec_ : Dec A → Dec B → Dec (A → B)

when, presumably (?), we should be consistent and instead write

------------------------------------------------------------------------
-- Interaction with negation, sum, product etc.

infixr 1 _⊎?_
infixr 2 _×?_ _→?_

T? : ∀ x → Dec (T x)
T? x = x because T-reflects x

¬? : Dec A → Dec (¬ A)
does  (¬? a?) = not (does a?)
proof (¬? a?) = ¬-reflects (proof a?)

⊤? : Dec {a} ⊤
does  ⊤? = true
proof ⊤? = ⊤-reflects

_×?_ : Dec A → Dec B → Dec (A × B)
does  (a? ×? b?) = does a? ∧ does b?
proof (a? ×? b?) = proof a? ×-reflects proof b?

⊥? : Dec {a} ⊥
does  ⊥?  = false
proof ⊥?  = ⊥-reflects

_⊎?_ : Dec A → Dec B → Dec (A ⊎ B)
does  (a? ⊎? b?) = does a? ∨ does b?
proof (a? ⊎? b?) = proof a? ⊎-reflects proof b?

_→?_ : Dec A → Dec B → Dec (A → B)
does  (a? →? b?) = not (does a?) ∨ does b?
proof (a? →? b?) = proof a? →-reflects proof b?

and deprecate the old names?

[JacquesCarette]

Agreed, ? names are nicer.

[jamesmckinna]

(moved to #2846 )