Merge pull request #146 from placidex/MetaM-minor-fixes

Add `set_option pp.explicit false` in Weak Head Normal Form example
leanprover-community · Sep 29, 2024 · 7246ae1 · 7246ae1
2 parents e474680 + 4ebc7ff
commit 7246ae1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean/main/04_metam.lean b/lean/main/04_metam.lean
@@ -566,7 +566,7 @@ we can see that the `+` notation amounts to an application of the `hAdd`
 function, which is a member of the `HAdd` typeclass:
 -/
 
-set_option pp.explicit true
+set_option pp.explicit true in
 #eval traceConstWithTransparency .reducible ``reducibleDef
 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) defaultDef 1