idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #3045 from mars0i/main

Browse Source 
Add documentation for Not.
This commit is contained in:
André Videla 2023-08-16 21:43:47 +09:00 committed by GitHub
commit 86c53e6071
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libs/prelude/Prelude/Basics.idr
View File

@ -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