5 Commits

Author	SHA1	Message	Date
Denis Buzdalov	874496e1ae	[base] Constructor's injectivity proofs for Exists and Subset (#1118) ... Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>	2021-02-24 19:11:41 +00:00
Denis Buzdalov	69be8f2102	[base] bimap functions were added for dependent pairs.	2021-02-24 16:41:33 +00:00
Denis Buzdalov	bcc8da5a6d	Currying and uncurrying functions for dependent pairs were added.	2021-01-15 18:53:40 +00:00
Denis Buzdalov	6d2dd935c4	Special variants of DPair as records (#922)	2021-01-15 17:19:20 +00:00
Jan de Muijnck-Hughes	874236aac0	A port of Subset and Exists from Idris1. ... The ports are rather straight forward and I have purposefully written the documentation to be beginner friendly. Note, I have diverged from Idris1 over the naming of the projection functions to make them consistent with `Pair` and `DPair`.	2020-07-04 11:03:14 +01:00