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
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20

def Array.insSort (A : Array Int32) := Id.run do
  let N := A.size
  let mut A := A
  for i in [:N] do
    for j in [:i] do
      -- Screw bounds checking
      -- I'm not afraid of segfaults
      if A[i - j]'(by sorry) < A[i - j - 1]'(by sorry) then
        A := A.swap (i - j - 1) (i - j) (by sorry) (by sorry)
      else
        break
  return A

-- Obviously that code is correct
theorem insSortCorrect : True := .intro

-- Actually let's test it just in case
#guard let A := #[69, 420, 1, 1, 13, 1, 65536]
  A.insSort = A.qsort
-- Yay it passed, so it must be correct