feat: add TransparencyMode.none

This PR adds a new transparency mode `.none` in which no definitions
are unfolded.

src/Init/MetaTypes.lean

@@ -36,6 +36,8 @@ inductive TransparencyMode where
   | reducible
   /-- Unfolds reducible constants and constants tagged with the `@[instance]` attribute. -/
   | instances
+  /-- Do not unfold anything -/
+  | none
   deriving Inhabited, BEq
 
 /-- Which structure types should eta be used with? -/

src/Lean/Elab/Tactic/Guard.lean

@@ -67,6 +67,7 @@ def MatchKind.toStringDescr : MatchKind → String
   | .defEq .all => s!"definitionally equal (unfolding all constants) to"
   | .defEq .reducible => s!"definitionally equal (unfolding reducible constants) to"
   | .defEq .instances => s!"definitionally equal (unfolding instances) to"
+  | .defEq .none => s!"definitionally equal (not unfolding any constants) to"
   | .alphaEq => "alpha-equivalent to"
 
 /-- Elaborate `a` and `b` and then do the given equality test `mk`. We make sure to unify

src/Lean/Meta/Basic.lean

@@ -34,6 +34,7 @@ def TransparencyMode.toUInt64 : TransparencyMode → UInt64
   | .default   => 1
   | .reducible => 2
   | .instances => 3
+  | .none      => 4
 
 def EtaStructMode.toUInt64 : EtaStructMode → UInt64
   | .all        => 0

src/Lean/Meta/GetUnfoldableConst.lean

@@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.GlobalInstances
-
 public section
-
 namespace Lean.Meta
 
 private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   match cfg.transparency with
-  | .all => return true
+  | .none => return false
+  | .all  => return true
   | .default => return !(← isIrreducible info.name)
   | m =>
     if (← isReducible info.name) then

src/Lean/Meta/Tactic/Congr.lean

@@ -112,7 +112,8 @@ def MVarId.congrN (mvarId : MVarId) (depth : Nat := 1000000) (closePre := true)
   return s.toList
 where
   post (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
-    if closePost && (← getTransparency) != .reducible then
+    let mode ← getTransparency
+    if closePost && mode != .reducible && mode != .none then
       if let some mvarId ← mvarId.congrPre then
         modify (·.push mvarId)
     else

src/Lean/Meta/TransparencyMode.lean

@@ -18,18 +18,34 @@ def hash : TransparencyMode → UInt64
   | default   => 11
   | reducible => 13
   | instances => 17
+  | none => 19
 
 instance : Hashable TransparencyMode := ⟨hash⟩
 
 def lt : TransparencyMode → TransparencyMode → Bool
-  | reducible, default   => true
-  | reducible, all       => true
-  | reducible, instances => true
-  | instances, default   => true
-  | instances, all       => true
+  | _,         none      => false
+  | none,      _         => true
+  | _,         reducible => false
+  | reducible, _         => true
+  | _,         instances => false
+  | instances, _         => true
   | default,   all       => true
   | _,         _         => false
 
 end TransparencyMode
 
+example (a b c : TransparencyMode) : a.lt b → b.lt c → a.lt c := by
+  cases a <;> cases b <;> cases c <;> simp [TransparencyMode.lt]
+
+example (a : TransparencyMode) : ¬ a.lt a := by
+  cases a <;> simp [TransparencyMode.lt]
+
+example (a b : TransparencyMode) : a.lt b → ¬ b.lt a := by
+  cases a <;> cases b <;> simp [TransparencyMode.lt]
+
+example : TransparencyMode.lt .none .reducible := rfl
+example : TransparencyMode.lt .reducible .instances := rfl
+example : TransparencyMode.lt .instances .default := rfl
+example : TransparencyMode.lt .default .all := rfl
+
 end Lean.Meta