aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Sigma.v
Commit message (Expand)AuthorAge
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
* Move sigma MapProjections to a separate fileGravatar Jason Gross2017-04-04
* Split off liftn_sig, add lift{3,4}_sigGravatar Jason Gross2017-04-03
* Add proj2_sig_mapGravatar Jason Gross2017-04-03
* Fix a typoGravatar Jason Gross2017-04-02
* Add projT2_mapGravatar Jason Gross2017-04-02
* Add η principles for sigma typesGravatar Jason Gross2017-03-01
* Added operation (including creating )Gravatar jadep2017-02-27
* Modified lemma and created tactic to handle it; added reduce step to multipl...Gravatar jadep2017-02-26
* Merge new base system (#112)Gravatar jadephilipoom2017-02-22
* Add inversion_exprGravatar Jason Gross2017-02-01
* Make [inversion_{prod,sigma}] strongerGravatar Jason Gross2016-09-05
* Add documentation: Equality, HProp, Isomorphism, Sigma (#41)Gravatar Jason Gross2016-08-01
* Remove useless hypotheses for [path_sigT_uncurried_iff]Gravatar Jason Gross2016-08-01
* Add inversion helper tactics to Sigma.vGravatar Jason Gross2016-07-29
* Rename path_sig{,T}{ => _uncurried}_iffGravatar Jason Gross2016-07-29
* Add path_sig{,T}_iffGravatar Jason Gross2016-07-29
* Add some lemmas to Util.SigmaGravatar Jason Gross2016-07-29
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 08:06:07 +0000