more tests

tests/addFalse/bad.lean

@@ -0,0 +1,17 @@
+import Batteries.Tactic.OpenPrivate
+
+open private mk from Lean.Environment
+
+open Lean in
+elab "add_false" : command => do
+  modifyEnv fun env =>
+    let constants := env.constants.insert `false $ ConstantInfo.thmInfo
+      { name := `false, levelParams := [], type := .const ``False [], value := .const ``False [] }
+    -- Before `Environment.mk` became private, we could just use
+    -- `{ env with constants }`
+    mk env.const2ModIdx constants env.extensions env.extraConstNames env.header
+
+add_false
+
+theorem falseThm : False :=
+   false

tests/addFalse/target.lean

@@ -0,0 +1,5 @@
+
+
+
+
+theorem falseThm : False := sorry

tests/addFalseConstr/bad.lean

@@ -0,0 +1,24 @@
+import Batteries.Tactic.OpenPrivate
+
+open private mk from Lean.Environment
+
+open Lean in
+elab "add_false_constructor" : command => do
+  modifyEnv fun env =>
+    let constants := env.constants.insert `False.intro $ ConstantInfo.ctorInfo
+      { name := `False.intro
+        levelParams := []
+        type := .const ``False []
+        induct := `False
+        cidx := 0
+        numParams := 0
+        numFields := 0
+        isUnsafe := false }
+    -- Before `Environment.mk` became private, we could just use
+    -- `{ env with constants }`
+    mk env.const2ModIdx constants env.extensions env.extraConstNames env.header
+
+add_false_constructor
+
+theorem falseThm : False :=
+  False.intro

tests/addFalseConstr/target.lean

@@ -0,0 +1,2 @@
+
+theorem falseThm : False := sorry