This one freezes F* at the last definition

Sandbox.fst

module Sandbox

module TC = FStar.Tactics.Typeclasses

class has_eq (t:Type) = {
  eq: t -> t -> bool;
  reflexivity : (x:t -> Lemma (eq x x));
  symmetry: (x:t -> y:t -> Lemma (requires eq x y) (ensures eq y x));
  transitivity: (x:t -> y:t -> z:t -> Lemma (requires (x `eq` y /\ y `eq` z)) (ensures (x `eq` z)))
} 

class has_mul (t:Type) = {  
  [@@@TC.no_method]
  haseq : has_eq t; 
  mul : t -> t -> t;
  [@@@TC.no_method]
  congruence: (x:t -> y:t -> z:t -> w:t -> Lemma (requires eq x z /\ eq y w) (ensures eq (mul x y) (mul z w)))
} 

class has_add (t:Type) = {  
  [@@@TC.no_method]
  haseq : has_eq t; 
  add : t -> t -> t;
  [@@@TC.no_method]
  congruence: (x:t -> y:t -> z:t -> w:t -> Lemma (requires eq x z /\ eq y w) (ensures eq (add x y) (add z w)));
  [@@@TC.no_method]
  commutativity: (x:t -> y:t -> Lemma (eq (add x y) (add y x)))
} 

instance ( + ) (#t:Type) {|a: has_add t|} = a.add
instance ( * ) (#t:Type) {|m: has_mul t|} = m.mul
instance ( = ) (#t:Type) {|h: has_eq t|} = h.eq
instance has_eq_of_mul (#t:Type) (h: has_mul t) = h.haseq

instance int_has_eq : has_eq int = {
  eq = op_Equality;
  reflexivity = (fun _ -> ());
  symmetry = (fun _ _ -> ());
  transitivity = (fun _ _ _ -> ())
}

class mul_semigroup (t:Type) = {
  [@@@TC.no_method]
  mul: has_mul t;
  associativity: (x:t -> y:t -> z:t -> Lemma ((x * y) * z = x * (y * z)))
}

class monoid (t:Type) = {
  [@@@TC.no_method]
  mul: mul_semigroup t;
  one: t;
  left_identity: (x:t -> Lemma ((one * x) = x))
}