- Jul 01, 2020
-
-
gabrielhdt authored -
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
- Jun 21, 2020
-
-
gabrielhdt authored
-
- Jun 20, 2020
-
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
Plus proof irrelevance for other casts
-
gabrielhdt authored
-
- Jun 17, 2020
-
-
gabrielhdt authored
downcast was unsound
-
gabrielhdt authored
-
gabrielhdt authored
- renamed subtype to subtype_poly - pi function does not have implicit arguments anymore - changed a rewrite rule into an axiom - added wip tuples
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
- Jun 03, 2020
-
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
- Jun 02, 2020
-
-
gabrielhdt authored
-
- May 27, 2020
-
-
gabrielhdt authored
-
- May 26, 2020
-
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
- May 22, 2020
-
-
gabrielhdt authored
-
- May 18, 2020
-
-
gabrielhdt authored
-
- May 17, 2020
-
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
- May 14, 2020
-
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
- May 11, 2020
-
-
gabrielhdt authored
-
gabrielhdt authored
-
- Apr 27, 2020
-
-
gabrielhdt authored
-
gabrielhdt authored
-
gabrielhdt authored
-
- Apr 23, 2020
-
-
gabrielhdt authored
-
- Apr 22, 2020
-
-
gabrielhdt authored
-