michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(arity): remove unnecessary implicit arguments

Browse source
This commit is contained in:
Floris van Doorn 2015-04-23 15:38:15 -04:00 committed by Leonardo de Moura
parent c1b23f29c9
commit cb5b07093f
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
hott/arity.hlean
View file

@ -134,8 +134,7 @@ namespace funext
begin
intro H, esimp [apD100, eq_of_homotopy2, function.compose],
apply eq_of_homotopy, intro a,
apply concat, apply (ap (λx, @apD10 _ (λb : B a, _) _ _ (x a))), apply (retr apD10),
--TODO: remove implicit argument after #469 is closed
apply concat, apply (ap (λx, apD10 (x a))), apply (retr apD10),
apply (retr apD10)
end
begin