Skip to content
Snippets Groups Projects
Commit 89ebe23f authored by Ralf Jung's avatar Ralf Jung
Browse files

Local Instance → Definition

parent eb035887
No related branches found
No related tags found
1 merge request!263Explicit visibility for Instances
Pipeline #47270 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/finite.v
+ 1
− 1
View file @ 89ebe23f
...@@ -237,7 +237,7 @@ Section bijective_finite. ...@@ -237,7 +237,7 @@ Section bijective_finite.
Context `{Finite A, EqDecision B} (f : A → B) (g : B → A). Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
Context `{!Inj (=) (=) f, !Cancel (=) f g}. Context `{!Inj (=) (=) f, !Cancel (=) f g}.
Local Instance bijective_finite: Finite B := Definition bijective_finite : Finite B :=
let _ := cancel_surj (f:=f) (g:=g) in let _ := cancel_surj (f:=f) (g:=g) in
surjective_finite f. surjective_finite f.
End bijective_finite. End bijective_finite.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment