feat(lean): add support for default methods

[clementblaudeau]

Rust offers default methods for traits, which can be overridden when writing implementations. Lean offers the same feature. This PR removes the rejection phase for default implementations, adds printing and testing for them.

trait T {
    fn dft(&self) -> usize {
        32
    }
}

// an impl can inherit the default values
impl T for u32 {}

// the default can also be overridden
impl T for usize {
    fn dft(&self) -> usize {
        self + 1
    }
}

class T (Self : Type) where
  dft (self : Self) : Result usize := do (pure (32 : usize))

instance Impl : T usize where
  dft (self : usize) := do (self +? (1 : usize))

instance Impl_1 : T u32 where
  -- no fields

Fixes https://github.com/cryspen/hax/issues/1707

[clementblaudeau]

Rebased on main.

[clementblaudeau]

(rebased on main)