feat: support define-sort command

[abdoo8080]

This PR implements one approach to supporting user-defined sorts (i.e., aliases): translating them into let expressions. The other approach is to eliminate them at the parser level. Note that the parser generated "letified" expression does not syntactically match the "letified" expression generated by Lean's elaborator:

/--
info: let i32 : Type := BitVec (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)));
∀ (x : i32),
  @Eq.{1} Bool
    (Bool.not
      (@bne.{0} (BitVec (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32))))
        (@instBEqOfDecidableEq.{0} (BitVec (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32))))
          (@instDecidableEqBitVec (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))))
        x
        (@Neg.neg.{0} (BitVec (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32))))
          (@BitVec.instNeg (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))) x)))
    Bool.true
-/
#guard_msgs in
set_option pp.all true in
#eval elabSexps sexps!{
(define-sort i32 () (_ BitVec 32))
(declare-fun x () i32)
(assert (distinct x (bvneg x)))
}

/--
info: let i32 : Type := BitVec (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)));
∀ (x : i32),
  @Eq.{1} Bool
    (Bool.not
      (@bne.{0} i32
        (@instBEqOfDecidableEq.{0} i32
          (@instDecidableEqBitVec (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))))
        x (@Neg.neg.{0} i32 (@BitVec.instNeg (@OfNat.ofNat.{0} Nat (nat_lit 32) (instOfNatNat (nat_lit 32)))) x)))
    Bool.true : Prop
-/
#guard_msgs in
set_option pp.all true in
#check let i32 := BitVec 32;
∀ (x : i32), (!x != -x) = true