fix(07): fix dependent pattern match

AndresTFG · Nov 25, 2016 · d4b8d62 · d4b8d62
1 parent 0fe1948
commit d4b8d62
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/07_Induction_and_Recursion.org b/07_Induction_and_Recursion.org
@@ -555,8 +555,8 @@ imf : Π a, image_of f (f a)
 
 open image_of
 
-definition inverse {f : A → B} : Π b, image_of f b → A
-| inverse ⌞f a⌟ (imf f a) := a
+definition inverse : Π f : A → B, Π b, image_of f b → A
+| inverse f ⌞f a⌟ (imf _ _) := a
 #+END_SRC
 
 Inaccessible terms can also be used to reduce the complexity of the