diff --git a/LeroyCompilerVerificationCourse/Compil.lean b/LeroyCompilerVerificationCourse/Compil.lean
index dd68bd6..00b5f49 100644
--- a/LeroyCompilerVerificationCourse/Compil.lean
+++ b/LeroyCompilerVerificationCourse/Compil.lean
@@ -124,6 +124,8 @@ def machine_goes_wrong (C: List instr) (s_init: store) : Prop :=
 def compile_program (p: com) : List instr:=
   compile_com p ++ .Ihalt :: []
 
+/-- info: [instr.Ivar "x", instr.Iconst 1, instr.Iadd, instr.Isetvar "x", instr.Ihalt] -/
+#guard_msgs in
 #eval (compile_program (.ASSIGN "x" (.PLUS (.VAR "x") (.CONST 1))))
 
 def smart_Ibranch (d: Int) : List instr:=
diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean
index eff2afa..02b01c2 100644
--- a/LeroyCompilerVerificationCourse/Constprop.lean
+++ b/LeroyCompilerVerificationCourse/Constprop.lean
@@ -47,6 +47,8 @@ set_option grind.warning false
   | .PLUS a1 a2 => mk_PLUS (simplif_aexp a1) (simplif_aexp a2)
   | .MINUS a1 a2 => mk_MINUS (simplif_aexp a1) (simplif_aexp a2)
 
+/-- info: aexp.MINUS (aexp.VAR "x") (aexp.VAR "y") -/
+#guard_msgs in
 #eval simplif_aexp (.MINUS (.PLUS (.VAR "x") (.CONST 1)) (.PLUS (.VAR "y") (.CONST 1)))
 
 @[grind] theorem mk_PLUS_CONST_sound:
diff --git a/LeroyCompilerVerificationCourse/Fixpoints.lean b/LeroyCompilerVerificationCourse/Fixpoints.lean
index 96f7fd4..b9da5e5 100644
--- a/LeroyCompilerVerificationCourse/Fixpoints.lean
+++ b/LeroyCompilerVerificationCourse/Fixpoints.lean
@@ -80,8 +80,6 @@ instance : WellFoundedRelation α  where
   decreasing_by
     grind [beq_false']
 
-#check iterate
-
 @[grind] theorem iterate_correct (x : α) (PRE: le x (F x)) (SMALL: forall z, le (F z) z -> le x z) (heq : y = iterate _ F x PRE SMALL ) : eq y (F y) ∧ ∀ z, le (F z) z → le y z := by
   fun_induction iterate
   case case1 x' PRE SMALL isTrue  =>
diff --git a/LeroyCompilerVerificationCourse/Imp.lean b/LeroyCompilerVerificationCourse/Imp.lean
index f9860f9..a3b2a91 100644
--- a/LeroyCompilerVerificationCourse/Imp.lean
+++ b/LeroyCompilerVerificationCourse/Imp.lean
@@ -18,6 +18,8 @@ def store : Type := ident → Int
   | .PLUS a1 a2 => aeval s a1 + aeval s a2
   | .MINUS a1 a2 => aeval s a1 - aeval s a2
 
+/-- info: 3 -/
+#guard_msgs in
 #eval aeval (λ _ => 2) (.PLUS (.VAR "x") (.MINUS (.VAR "x") (.CONST 1)))
 
 theorem aeval_xplus1 : ∀ s x, aeval s (.PLUS (.VAR x) (.CONST 1)) > aeval s (.VAR x) := by
@@ -76,8 +78,6 @@ inductive com: Type where
 
 notation:10 l:10 " ;; " r:11 => com.SEQ l r
 
-#check .SKIP ;; .SKIP
-
 def Euclidean_division :=
   .ASSIGN "r" (.VAR "a") ;;
   .ASSIGN "q" (.CONST 0) ;;