From bdb6531b860de2ebe64e6a2ddbb6fe7b34eb1288 Mon Sep 17 00:00:00 2001
From: Marshall Abrams <marshall@logical.net>
Date: Mon, 14 Aug 2023 22:44:07 -0500
Subject: [PATCH] Add documentation for Not.

---
 libs/prelude/Prelude/Basics.idr | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr
index 87ad2e50ee..0e04864e3e 100644
--- a/libs/prelude/Prelude/Basics.idr
+++ b/libs/prelude/Prelude/Basics.idr
@@ -6,6 +6,10 @@ import Prelude.Ops
 
 %default total
 
+
+||| `Not x` is an alias for `x -> Void`, indicating that any term of type `x`
+||| leads to a contradiction. It can be used in conjunction with `void` or
+||| `absurd`.
 public export
 Not : Type -> Type
 Not x = x -> Void