max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: more general instance

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-01 09:16:29 -08:00
parent dd4bed3c6f
commit d37d02b512
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Control/Except.lean
View file

@ -18,7 +18,7 @@ inductive Except (ε : Type u) (α : Type v)
attribute [unbox] Except
instance {ε α : Type} [Inhabited ε] : Inhabited (Except ε α) :=
instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) :=
⟨Except.error (arbitrary ε)⟩
section