@@ -88,9 +88,9 @@ error:
89 When elaborating right hand side of four_eq_five:
89 When elaborating right hand side of four_eq_five:
90 Can't unify
90 Can't unify
91− 5 = 5
91+ x = x (Type of Refl)
93− 4 = 5
93+ 4 = 5 (Expected type)
95Type checking equality proofs
95Type checking equality proofs
96~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
96~~~~~~~~~~~~~~~~~~~~~~~~~~~~~