1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14

-- This works
/-- Moo. -/
@[inline]
def moo (a : Nat) := a

-- This doesn't
@[inline]
/-- Moo. -/
def moo2 (a : Nat) := a

open scoped Classical in
/-- Moo. -/
@[inline]
def moo3 (a : Nat) := a