| /- | |
| Copyright (c) 2021 Gabriel Ebner. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Gabriel Ebner, Mario Carneiro | |
| -/ | |
| prelude | |
| import Init.Core | |
| /-! | |
| Instances converting between `Zero α` and `OfNat α (nat_lit 0)`. | |
| -/ | |
| instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where | |
| ofNat := ‹Zero α›.1 | |
| instance (priority := 200) Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where | |
| zero := 0 |