def m : Nat := 0

이거 하려는데

unknown identifier 'Nat'이라네

임포트라도 해줘야하나 싶어서 자동완성으로 init.data.nat을 찾긴 했는데
얜 nat인가봄..

구글링해봐도 암것도 안나오는데 도움좀