6ebe573c19
This PR moves the universe-level-count check from `unfold_definition_core` into `is_delta`, establishing the invariant that if `is_delta` succeeds then `unfold_definition` also succeeds. This prevents a crash (SIGSEGV or garbled error) that occurred when call sites in `lazy_delta_reduction_step` unconditionally dereferenced the result of `unfold_definition` even on a level-parameter-count mismatch. Additionally, moves the `is_prop` check for theorem types in `add_theorem` to occur after `check_constant_val`, so the type is verified to be well-formed before `is_prop` evaluates it. This prevents `is_prop` from being called on an ill-typed term when a malformed theorem declaration is supplied. Fixes #10577. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: nomeata <148037+nomeata@users.noreply.github.com>
643 lines
31 KiB
Text
643 lines
31 KiB
Text
import Lean
|
|
def decodeNatLit (l : List Nat) : Nat := l.foldl (init := 0) (fun sofar d => 256 * sofar + d)
|
|
def name_0 : Lean.Name := .anonymous
|
|
def level_0 : Lean.Level := .zero
|
|
def name_1 : Lean.Name := .str name_0 "term_+_"
|
|
def level_1 : Lean.Level := .param name_1
|
|
def level_2 : Lean.Level := .succ level_1
|
|
def expr_0 : Lean.Expr := .sort level_2
|
|
def expr_1 : Lean.Expr := .bvar 0
|
|
def name_2 : Lean.Name := .str name_0 "_sizeOf_1"
|
|
def expr_2 : Lean.Expr := .const name_2 [level_1]
|
|
def expr_3 : Lean.Expr := .bvar 1
|
|
def expr_4 : Lean.Expr := .app expr_2 expr_3
|
|
def name_3 : Lean.Name := .str name_0 "term_+_"
|
|
def name_4 : Lean.Name := .str name_0 "term_+_"
|
|
def name_5 : Lean.Name := .str name_1 "term_+_"
|
|
def name_6 : Lean.Name := .str name_0 "term_+_"
|
|
def name_7 : Lean.Name := .str name_2 "term_+_"
|
|
def name_8 : Lean.Name := .str name_0 "term_+_"
|
|
def expr_5 : Lean.Expr := .forallE name_6 expr_1 expr_4 .default
|
|
def name_9 : Lean.Name := .str name_6 "term_+_"
|
|
def expr_6 : Lean.Expr := .forallE name_6 expr_0 expr_5 .default
|
|
def name_10 : Lean.Name := .str name_6 "term_+_"
|
|
def constructor_0 : Lean.Constructor where
|
|
name := name_10
|
|
type := expr_6
|
|
def name_11 : Lean.Name := .str name_5 "term_+_"
|
|
def expr_7 : Lean.Expr := .forallE name_0 expr_5 expr_4 .default
|
|
def expr_8 : Lean.Expr := .forallE name_0 expr_0 expr_7 .default
|
|
def name_12 : Lean.Name := .str name_0 "ε'"
|
|
def constructor_1 : Lean.Constructor where
|
|
name := name_12
|
|
type := expr_8
|
|
def expr_9 : Lean.Expr := .forallE name_12 expr_0 expr_0 .default
|
|
def inductive_0 : Lean.InductiveType where
|
|
name := name_2
|
|
type := expr_9
|
|
ctors := [constructor_0, constructor_1]
|
|
def decl_0 : Lean.Declaration :=
|
|
.inductDecl [name_4] 1 [inductive_0] false
|
|
def name_13 : Lean.Name := .str name_2 "rec"
|
|
def expr_10 : Lean.Expr := .app expr_2 expr_1
|
|
def name_14 : Lean.Name := .str name_2 "term_+_"
|
|
def level_3 : Lean.Level := .param name_14
|
|
def expr_11 : Lean.Expr := .sort level_3
|
|
def name_15 : Lean.Name := .str name_6 "term_+_"
|
|
def expr_12 : Lean.Expr := .forallE name_0 expr_10 expr_11 .default
|
|
def expr_13 : Lean.Expr := .bvar 2
|
|
def expr_14 : Lean.Expr := .const name_10 [level_1]
|
|
def expr_15 : Lean.Expr := .bvar 3
|
|
def expr_16 : Lean.Expr := .app expr_14 expr_15
|
|
def expr_17 : Lean.Expr := .app expr_16 expr_1
|
|
def expr_18 : Lean.Expr := .app expr_13 expr_17
|
|
def expr_19 : Lean.Expr := .forallE name_0 expr_13 expr_18 .default
|
|
def expr_20 : Lean.Expr := .bvar 4
|
|
def expr_21 : Lean.Expr := .app expr_2 expr_20
|
|
def name_16 : Lean.Name := .str name_0 "term_+_"
|
|
def expr_22 : Lean.Expr := .forallE name_11 expr_15 expr_21 .default
|
|
def expr_23 : Lean.Expr := .const name_12 [level_1]
|
|
def expr_24 : Lean.Expr := .app expr_23 expr_20
|
|
def expr_25 : Lean.Expr := .app expr_24 expr_1
|
|
def expr_26 : Lean.Expr := .app expr_15 expr_25
|
|
def expr_27 : Lean.Expr := .forallE name_11 expr_22 expr_26 .default
|
|
def expr_28 : Lean.Expr := .app expr_15 expr_13
|
|
def name_17 : Lean.Name := .str name_11 "term_+_"
|
|
def expr_29 : Lean.Expr := .forallE name_6 expr_27 expr_28 .default
|
|
def name_18 : Lean.Name := .str name_6 "term_+_"
|
|
def expr_30 : Lean.Expr := .forallE name_5 expr_19 expr_29 .default
|
|
def expr_31 : Lean.Expr := .forallE name_5 expr_4 expr_30 .default
|
|
def name_19 : Lean.Name := .str name_5 "term_+_"
|
|
def expr_32 : Lean.Expr := .forallE name_16 expr_12 expr_31 .default
|
|
def expr_33 : Lean.Expr := .forallE name_16 expr_0 expr_32 .default
|
|
def expr_34 : Lean.Expr := .const name_13 [level_3, level_1]
|
|
def expr_35 : Lean.Expr := .app expr_34 expr_20
|
|
def expr_36 : Lean.Expr := .app expr_35 expr_15
|
|
def expr_37 : Lean.Expr := .app expr_13 expr_1
|
|
def expr_38 : Lean.Expr := .lam name_16 expr_20 expr_37 .default
|
|
def expr_39 : Lean.Expr := .app expr_36 expr_38
|
|
def expr_40 : Lean.Expr := .bvar 5
|
|
def expr_41 : Lean.Expr := .app expr_2 expr_40
|
|
def expr_42 : Lean.Expr := .forallE name_16 expr_20 expr_41 .default
|
|
def expr_43 : Lean.Expr := .app expr_3 expr_1
|
|
def expr_44 : Lean.Expr := .app expr_40 expr_43
|
|
def expr_45 : Lean.Expr := .forallE name_16 expr_40 expr_44 .default
|
|
def expr_46 : Lean.Expr := .app expr_13 expr_3
|
|
def name_20 : Lean.Name := .str name_16 "term_+_"
|
|
def name_21 : Lean.Name := .str name_9 "term_+_"
|
|
def name_22 : Lean.Name := .str name_16 "term_+_"
|
|
def name_23 : Lean.Name := .str name_8 "term_+_"
|
|
def name_24 : Lean.Name := .str name_0 "term_+_"
|
|
def name_25 : Lean.Name := .str name_11 "term_+_"
|
|
def expr_47 : Lean.Expr := .lam name_12 expr_45 expr_46 .default
|
|
def expr_48 : Lean.Expr := .lam name_12 expr_42 expr_47 .default
|
|
def expr_49 : Lean.Expr := .app expr_39 expr_48
|
|
def expr_50 : Lean.Expr := .app expr_49 expr_13
|
|
def expr_51 : Lean.Expr := .lam name_12 expr_27 expr_50 .default
|
|
def expr_52 : Lean.Expr := .lam name_12 expr_19 expr_51 .default
|
|
def expr_53 : Lean.Expr := .lam name_12 expr_4 expr_52 .default
|
|
def expr_54 : Lean.Expr := .lam name_12 expr_12 expr_53 .default
|
|
def expr_55 : Lean.Expr := .lam name_12 expr_0 expr_54 .default
|
|
def name_26 : Lean.Name := .str name_12 "term_+_"
|
|
def decl_1 : Lean.Declaration :=
|
|
.defnDecl {
|
|
name := name_26
|
|
levelParams := [name_14, name_24]
|
|
type := expr_33
|
|
value := expr_55
|
|
hints := .opaque
|
|
safety := .safe
|
|
all := [name_26]
|
|
}
|
|
def expr_56 : Lean.Expr := .app expr_2 expr_13
|
|
def name_27 : Lean.Name := .str name_24 "term_+_"
|
|
def expr_57 : Lean.Expr := .forallE name_16 expr_56 expr_11 .default
|
|
def name_28 : Lean.Name := .str name_16 "term_+_"
|
|
def expr_58 : Lean.Expr := .forallE name_11 expr_4 expr_57 .default
|
|
def name_29 : Lean.Name := .str name_11 "term_+_"
|
|
def expr_59 : Lean.Expr := .forallE name_6 expr_11 expr_58 .default
|
|
def expr_60 : Lean.Expr := .forallE name_6 expr_0 expr_59 .default
|
|
def level_4 : Lean.Level := .succ level_3
|
|
def expr_61 : Lean.Expr := .const name_26 [level_4, level_1]
|
|
def expr_62 : Lean.Expr := .app expr_61 expr_15
|
|
def expr_63 : Lean.Expr := .app expr_2 expr_15
|
|
def expr_64 : Lean.Expr := .lam name_6 expr_63 expr_11 .default
|
|
def expr_65 : Lean.Expr := .app expr_62 expr_64
|
|
def expr_66 : Lean.Expr := .app expr_65 expr_3
|
|
def expr_67 : Lean.Expr := .app expr_61 expr_20
|
|
def expr_68 : Lean.Expr := .lam name_6 expr_21 expr_11 .default
|
|
def expr_69 : Lean.Expr := .app expr_67 expr_68
|
|
def expr_70 : Lean.Expr := .app expr_69 expr_3
|
|
def name_30 : Lean.Name := .str name_0 "Eq"
|
|
def expr_71 : Lean.Expr := .const name_30 [level_2]
|
|
def expr_72 : Lean.Expr := .app expr_71 expr_40
|
|
def expr_73 : Lean.Expr := .app expr_72 expr_3
|
|
def expr_74 : Lean.Expr := .app expr_73 expr_1
|
|
def name_31 : Lean.Name := .str name_29 "term_+_"
|
|
def name_32 : Lean.Name := .str name_16 "term_+_"
|
|
def name_33 : Lean.Name := .str name_27 "term_+_"
|
|
def name_34 : Lean.Name := .str name_28 "term_+_"
|
|
def name_35 : Lean.Name := .str name_16 "term_+_"
|
|
def name_36 : Lean.Name := .str name_24 "term_+_"
|
|
def expr_75 : Lean.Expr := .forallE name_15 expr_74 expr_40 .default
|
|
def expr_76 : Lean.Expr := .forallE name_15 expr_75 expr_40 .default
|
|
def expr_77 : Lean.Expr := .lam name_15 expr_20 expr_76 .default
|
|
def expr_78 : Lean.Expr := .app expr_70 expr_77
|
|
def expr_79 : Lean.Expr := .lam name_15 expr_42 expr_20 .default
|
|
def expr_80 : Lean.Expr := .app expr_78 expr_79
|
|
def expr_81 : Lean.Expr := .lam name_15 expr_15 expr_80 .default
|
|
def expr_82 : Lean.Expr := .app expr_66 expr_81
|
|
def expr_83 : Lean.Expr := .lam name_15 expr_20 expr_20 .default
|
|
def expr_84 : Lean.Expr := .app expr_70 expr_83
|
|
def expr_85 : Lean.Expr := .bvar 6
|
|
def expr_86 : Lean.Expr := .app expr_2 expr_85
|
|
def expr_87 : Lean.Expr := .forallE name_15 expr_40 expr_86 .default
|
|
def expr_88 : Lean.Expr := .app expr_71 expr_87
|
|
def expr_89 : Lean.Expr := .app expr_88 expr_3
|
|
def expr_90 : Lean.Expr := .app expr_89 expr_1
|
|
def name_37 : Lean.Name := .str name_15 "term_+_"
|
|
def expr_91 : Lean.Expr := .forallE name_24 expr_90 expr_40 .default
|
|
def expr_92 : Lean.Expr := .forallE name_24 expr_91 expr_40 .default
|
|
def expr_93 : Lean.Expr := .lam name_24 expr_42 expr_92 .default
|
|
def expr_94 : Lean.Expr := .app expr_84 expr_93
|
|
def expr_95 : Lean.Expr := .lam name_24 expr_22 expr_94 .default
|
|
def expr_96 : Lean.Expr := .app expr_82 expr_95
|
|
def expr_97 : Lean.Expr := .lam name_24 expr_56 expr_96 .default
|
|
def expr_98 : Lean.Expr := .lam name_24 expr_4 expr_97 .default
|
|
def expr_99 : Lean.Expr := .lam name_24 expr_11 expr_98 .default
|
|
def expr_100 : Lean.Expr := .lam name_24 expr_0 expr_99 .default
|
|
def name_38 : Lean.Name := .str name_24 "inj"
|
|
def decl_2 : Lean.Declaration :=
|
|
.defnDecl {
|
|
name := name_38
|
|
levelParams := [name_14, name_4]
|
|
type := expr_60
|
|
value := expr_100
|
|
hints := .opaque
|
|
safety := .safe
|
|
all := [name_38]
|
|
}
|
|
def expr_101 : Lean.Expr := .sort level_4
|
|
def expr_102 : Lean.Expr := .const name_2 [level_3]
|
|
def expr_103 : Lean.Expr := .app expr_102 expr_1
|
|
def name_39 : Lean.Name := .str name_12 "term_+_"
|
|
def level_5 : Lean.Level := .succ level_3
|
|
def expr_104 : Lean.Expr := .sort level_5
|
|
def name_40 : Lean.Name := .str name_16 "term_+_"
|
|
def name_41 : Lean.Name := .str name_36 "term_+_"
|
|
def name_42 : Lean.Name := .str name_30 "term_+_"
|
|
def name_43 : Lean.Name := .str name_38 "term_+_"
|
|
def name_44 : Lean.Name := .str name_16 "term_+_"
|
|
def name_45 : Lean.Name := .str name_6 "term_+_"
|
|
def name_46 : Lean.Name := .str name_8 "term_+_"
|
|
def expr_105 : Lean.Expr := .forallE name_22 expr_103 expr_104 .default
|
|
def expr_106 : Lean.Expr := .app expr_102 expr_3
|
|
def expr_107 : Lean.Expr := .const name_10 [level_3]
|
|
def expr_108 : Lean.Expr := .app expr_107 expr_15
|
|
def expr_109 : Lean.Expr := .app expr_108 expr_1
|
|
def expr_110 : Lean.Expr := .app expr_13 expr_109
|
|
def name_47 : Lean.Name := .str name_22 "term_+_"
|
|
def expr_111 : Lean.Expr := .forallE name_0 expr_13 expr_110 .default
|
|
def expr_112 : Lean.Expr := .app expr_102 expr_20
|
|
def expr_113 : Lean.Expr := .forallE name_0 expr_15 expr_112 .default
|
|
def expr_114 : Lean.Expr := .const name_12 [level_3]
|
|
def expr_115 : Lean.Expr := .app expr_114 expr_20
|
|
def expr_116 : Lean.Expr := .app expr_115 expr_1
|
|
def expr_117 : Lean.Expr := .app expr_15 expr_116
|
|
def name_48 : Lean.Name := .str name_0 "term_+_"
|
|
def expr_118 : Lean.Expr := .forallE name_37 expr_113 expr_117 .default
|
|
def name_49 : Lean.Name := .str name_37 "term_+_"
|
|
def expr_119 : Lean.Expr := .forallE name_36 expr_118 expr_28 .default
|
|
def name_50 : Lean.Name := .str name_36 "term_+_"
|
|
def expr_120 : Lean.Expr := .forallE name_45 expr_111 expr_119 .default
|
|
def expr_121 : Lean.Expr := .forallE name_45 expr_106 expr_120 .default
|
|
def expr_122 : Lean.Expr := .forallE name_45 expr_105 expr_121 .default
|
|
def expr_123 : Lean.Expr := .forallE name_45 expr_101 expr_122 .default
|
|
def expr_124 : Lean.Expr := .const name_26 [level_5, level_3]
|
|
def expr_125 : Lean.Expr := .app expr_124 expr_20
|
|
def expr_126 : Lean.Expr := .app expr_20 expr_1
|
|
def expr_127 : Lean.Expr := .lam name_45 expr_112 expr_126 .default
|
|
def expr_128 : Lean.Expr := .app expr_125 expr_127
|
|
def expr_129 : Lean.Expr := .app expr_128 expr_13
|
|
def expr_130 : Lean.Expr := .app expr_129 expr_38
|
|
def expr_131 : Lean.Expr := .app expr_102 expr_40
|
|
def expr_132 : Lean.Expr := .forallE name_45 expr_20 expr_131 .default
|
|
def name_51 : Lean.Name := .str name_45 "term_+_"
|
|
def expr_133 : Lean.Expr := .lam name_12 expr_132 expr_43 .default
|
|
def expr_134 : Lean.Expr := .app expr_130 expr_133
|
|
def expr_135 : Lean.Expr := .lam name_12 expr_118 expr_134 .default
|
|
def expr_136 : Lean.Expr := .lam name_12 expr_111 expr_135 .default
|
|
def expr_137 : Lean.Expr := .lam name_12 expr_106 expr_136 .default
|
|
def expr_138 : Lean.Expr := .lam name_12 expr_105 expr_137 .default
|
|
def expr_139 : Lean.Expr := .lam name_12 expr_101 expr_138 .default
|
|
def name_52 : Lean.Name := .str name_12 "term_+_"
|
|
def name_53 : Lean.Name := .str name_40 "term_+_"
|
|
def decl_3 : Lean.Declaration :=
|
|
.defnDecl {
|
|
name := name_29
|
|
levelParams := [name_14, name_24]
|
|
type := expr_123
|
|
value := expr_139
|
|
hints := .opaque
|
|
safety := .safe
|
|
all := [name_29]
|
|
}
|
|
def expr_140 : Lean.Expr := .app expr_71 expr_63
|
|
def expr_141 : Lean.Expr := .app expr_140 expr_3
|
|
def expr_142 : Lean.Expr := .app expr_141 expr_1
|
|
def expr_143 : Lean.Expr := .const name_38 [level_3, level_1]
|
|
def expr_144 : Lean.Expr := .app expr_143 expr_20
|
|
def expr_145 : Lean.Expr := .app expr_144 expr_15
|
|
def expr_146 : Lean.Expr := .app expr_145 expr_13
|
|
def expr_147 : Lean.Expr := .app expr_146 expr_3
|
|
def name_54 : Lean.Name := .str name_24 "term_+_"
|
|
def expr_148 : Lean.Expr := .forallE name_16 expr_142 expr_147 .default
|
|
def expr_149 : Lean.Expr := .forallE name_16 expr_56 expr_148 .default
|
|
def expr_150 : Lean.Expr := .forallE name_16 expr_4 expr_149 .default
|
|
def expr_151 : Lean.Expr := .forallE name_16 expr_11 expr_150 .default
|
|
def expr_152 : Lean.Expr := .forallE name_16 expr_0 expr_151 .default
|
|
def name_55 : Lean.Name := .str name_30 "ndrec"
|
|
def expr_153 : Lean.Expr := .const name_55 [level_3, level_2]
|
|
def expr_154 : Lean.Expr := .app expr_153 expr_21
|
|
def expr_155 : Lean.Expr := .app expr_154 expr_13
|
|
def expr_156 : Lean.Expr := .app expr_71 expr_41
|
|
def expr_157 : Lean.Expr := .app expr_156 expr_15
|
|
def expr_158 : Lean.Expr := .app expr_157 expr_1
|
|
def expr_159 : Lean.Expr := .app expr_143 expr_85
|
|
def expr_160 : Lean.Expr := .app expr_159 expr_40
|
|
def expr_161 : Lean.Expr := .app expr_160 expr_20
|
|
def expr_162 : Lean.Expr := .app expr_161 expr_3
|
|
def name_56 : Lean.Name := .str name_16 "term_+_"
|
|
def expr_163 : Lean.Expr := .forallE name_24 expr_158 expr_162 .default
|
|
def expr_164 : Lean.Expr := .lam name_24 expr_21 expr_163 .default
|
|
def expr_165 : Lean.Expr := .app expr_155 expr_164
|
|
def expr_166 : Lean.Expr := .app expr_71 expr_21
|
|
def expr_167 : Lean.Expr := .app expr_166 expr_13
|
|
def expr_168 : Lean.Expr := .app expr_167 expr_13
|
|
def expr_169 : Lean.Expr := .const name_26 [level_3, level_1]
|
|
def expr_170 : Lean.Expr := .app expr_169 expr_40
|
|
def expr_171 : Lean.Expr := .app expr_160 expr_1
|
|
def expr_172 : Lean.Expr := .app expr_171 expr_1
|
|
def expr_173 : Lean.Expr := .lam name_24 expr_41 expr_172 .default
|
|
def expr_174 : Lean.Expr := .app expr_170 expr_173
|
|
def expr_175 : Lean.Expr := .app expr_174 expr_15
|
|
def expr_176 : Lean.Expr := .app expr_71 expr_85
|
|
def expr_177 : Lean.Expr := .app expr_176 expr_1
|
|
def expr_178 : Lean.Expr := .app expr_177 expr_1
|
|
def expr_179 : Lean.Expr := .forallE name_24 expr_178 expr_85 .default
|
|
def name_57 : Lean.Name := .str name_30 "refl"
|
|
def expr_180 : Lean.Expr := .const name_57 [level_2]
|
|
def expr_181 : Lean.Expr := .bvar 7
|
|
def expr_182 : Lean.Expr := .app expr_180 expr_181
|
|
def expr_183 : Lean.Expr := .app expr_182 expr_3
|
|
def expr_184 : Lean.Expr := .app expr_1 expr_183
|
|
def expr_185 : Lean.Expr := .lam name_40 expr_179 expr_184 .default
|
|
def expr_186 : Lean.Expr := .lam name_40 expr_40 expr_185 .default
|
|
def expr_187 : Lean.Expr := .app expr_175 expr_186
|
|
def expr_188 : Lean.Expr := .app expr_2 expr_181
|
|
def expr_189 : Lean.Expr := .forallE name_40 expr_85 expr_188 .default
|
|
def expr_190 : Lean.Expr := .app expr_71 expr_189
|
|
def expr_191 : Lean.Expr := .app expr_190 expr_1
|
|
def expr_192 : Lean.Expr := .app expr_191 expr_1
|
|
def expr_193 : Lean.Expr := .forallE name_40 expr_192 expr_85 .default
|
|
def expr_194 : Lean.Expr := .bvar 8
|
|
def expr_195 : Lean.Expr := .app expr_2 expr_194
|
|
def expr_196 : Lean.Expr := .forallE name_40 expr_181 expr_195 .default
|
|
def expr_197 : Lean.Expr := .app expr_180 expr_196
|
|
def expr_198 : Lean.Expr := .app expr_197 expr_3
|
|
def expr_199 : Lean.Expr := .app expr_1 expr_198
|
|
def expr_200 : Lean.Expr := .lam name_40 expr_193 expr_199 .default
|
|
def expr_201 : Lean.Expr := .lam name_40 expr_87 expr_200 .default
|
|
def expr_202 : Lean.Expr := .app expr_187 expr_201
|
|
def name_58 : Lean.Name := .str name_40 "term_+_"
|
|
def expr_203 : Lean.Expr := .lam name_5 expr_168 expr_202 .default
|
|
def expr_204 : Lean.Expr := .app expr_165 expr_203
|
|
def expr_205 : Lean.Expr := .app expr_204 expr_3
|
|
def expr_206 : Lean.Expr := .app expr_205 expr_1
|
|
def expr_207 : Lean.Expr := .app expr_206 expr_1
|
|
def expr_208 : Lean.Expr := .lam name_5 expr_142 expr_207 .default
|
|
def expr_209 : Lean.Expr := .lam name_5 expr_56 expr_208 .default
|
|
def expr_210 : Lean.Expr := .lam name_5 expr_4 expr_209 .default
|
|
def expr_211 : Lean.Expr := .lam name_5 expr_11 expr_210 .default
|
|
def expr_212 : Lean.Expr := .lam name_5 expr_0 expr_211 .default
|
|
def name_59 : Lean.Name := .str name_5 "term_+_"
|
|
def decl_4 : Lean.Declaration :=
|
|
.defnDecl {
|
|
name := name_47
|
|
levelParams := [name_14, name_48]
|
|
type := expr_152
|
|
value := expr_212
|
|
hints := .opaque
|
|
safety := .safe
|
|
all := [name_47]
|
|
}
|
|
def expr_213 : Lean.Expr := .forallE name_36 expr_10 expr_101 .default
|
|
def level_6 : Lean.Level := .max level_4 level_2
|
|
def expr_214 : Lean.Expr := .sort level_6
|
|
def expr_215 : Lean.Expr := .forallE name_36 expr_4 expr_214 .default
|
|
def expr_216 : Lean.Expr := .forallE name_36 expr_213 expr_215 .default
|
|
def expr_217 : Lean.Expr := .forallE name_36 expr_0 expr_216 .default
|
|
def level_7 : Lean.Level := .succ level_6
|
|
def expr_218 : Lean.Expr := .const name_13 [level_7, level_1]
|
|
def expr_219 : Lean.Expr := .app expr_218 expr_13
|
|
def expr_220 : Lean.Expr := .lam name_36 expr_56 expr_214 .default
|
|
def expr_221 : Lean.Expr := .app expr_219 expr_220
|
|
def name_60 : Lean.Name := .str name_0 "PUnit"
|
|
def expr_222 : Lean.Expr := .const name_60 [level_6]
|
|
def expr_223 : Lean.Expr := .lam name_14 expr_13 expr_222 .default
|
|
def expr_224 : Lean.Expr := .app expr_221 expr_223
|
|
def expr_225 : Lean.Expr := .forallE name_14 expr_13 expr_63 .default
|
|
def expr_226 : Lean.Expr := .forallE name_14 expr_15 expr_214 .default
|
|
def name_61 : Lean.Name := .str name_0 "PProd"
|
|
def level_8 : Lean.Level := .max level_2 level_4
|
|
def expr_227 : Lean.Expr := .const name_61 [level_8, level_8]
|
|
def expr_228 : Lean.Expr := .app expr_20 expr_37
|
|
def expr_229 : Lean.Expr := .forallE name_60 expr_20 expr_228 .default
|
|
def expr_230 : Lean.Expr := .app expr_227 expr_229
|
|
def expr_231 : Lean.Expr := .forallE name_60 expr_20 expr_43 .default
|
|
def expr_232 : Lean.Expr := .app expr_230 expr_231
|
|
def expr_233 : Lean.Expr := .lam name_60 expr_226 expr_232 .default
|
|
def expr_234 : Lean.Expr := .lam name_60 expr_225 expr_233 .default
|
|
def expr_235 : Lean.Expr := .app expr_224 expr_234
|
|
def expr_236 : Lean.Expr := .app expr_235 expr_1
|
|
def expr_237 : Lean.Expr := .lam name_60 expr_4 expr_236 .default
|
|
def expr_238 : Lean.Expr := .lam name_60 expr_213 expr_237 .default
|
|
def expr_239 : Lean.Expr := .lam name_60 expr_0 expr_238 .default
|
|
def name_62 : Lean.Name := .str name_60 "below"
|
|
def decl_5 : Lean.Declaration :=
|
|
.defnDecl {
|
|
name := name_62
|
|
levelParams := [name_14, name_4]
|
|
type := expr_217
|
|
value := expr_239
|
|
hints := .opaque
|
|
safety := .safe
|
|
all := [name_62]
|
|
}
|
|
def expr_240 : Lean.Expr := .sort level_0
|
|
def expr_241 : Lean.Expr := .forallE name_51 expr_10 expr_240 .default
|
|
def expr_242 : Lean.Expr := .forallE name_51 expr_4 expr_240 .default
|
|
def expr_243 : Lean.Expr := .forallE name_51 expr_241 expr_242 .default
|
|
def expr_244 : Lean.Expr := .forallE name_51 expr_0 expr_243 .default
|
|
def level_9 : Lean.Level := .succ level_0
|
|
def expr_245 : Lean.Expr := .const name_13 [level_9, level_1]
|
|
def expr_246 : Lean.Expr := .app expr_245 expr_13
|
|
def expr_247 : Lean.Expr := .lam name_51 expr_56 expr_240 .default
|
|
def expr_248 : Lean.Expr := .app expr_246 expr_247
|
|
def name_63 : Lean.Name := .str name_0 "True"
|
|
def expr_249 : Lean.Expr := .const name_63 []
|
|
def expr_250 : Lean.Expr := .lam name_48 expr_13 expr_249 .default
|
|
def expr_251 : Lean.Expr := .app expr_248 expr_250
|
|
def expr_252 : Lean.Expr := .forallE name_48 expr_15 expr_240 .default
|
|
def name_64 : Lean.Name := .str name_0 "And"
|
|
def expr_253 : Lean.Expr := .const name_64 []
|
|
def expr_254 : Lean.Expr := .app expr_253 expr_229
|
|
def expr_255 : Lean.Expr := .app expr_254 expr_231
|
|
def expr_256 : Lean.Expr := .lam name_51 expr_252 expr_255 .default
|
|
def expr_257 : Lean.Expr := .lam name_51 expr_225 expr_256 .default
|
|
def expr_258 : Lean.Expr := .app expr_251 expr_257
|
|
def expr_259 : Lean.Expr := .app expr_258 expr_1
|
|
def expr_260 : Lean.Expr := .lam name_51 expr_4 expr_259 .default
|
|
def expr_261 : Lean.Expr := .lam name_51 expr_241 expr_260 .default
|
|
def expr_262 : Lean.Expr := .lam name_51 expr_0 expr_261 .default
|
|
def name_65 : Lean.Name := .str name_51 "casesOn"
|
|
def decl_6 : Lean.Declaration :=
|
|
.defnDecl {
|
|
name := name_65
|
|
levelParams := [name_48]
|
|
type := expr_244
|
|
value := expr_262
|
|
hints := .opaque
|
|
safety := .safe
|
|
all := [name_65]
|
|
}
|
|
def expr_263 : Lean.Expr := .const name_65 [level_1]
|
|
def expr_264 : Lean.Expr := .app expr_263 expr_15
|
|
def expr_265 : Lean.Expr := .app expr_264 expr_13
|
|
def expr_266 : Lean.Expr := .app expr_265 expr_1
|
|
def expr_267 : Lean.Expr := .app expr_15 expr_3
|
|
def expr_268 : Lean.Expr := .forallE name_60 expr_266 expr_267 .default
|
|
def expr_269 : Lean.Expr := .forallE name_60 expr_56 expr_268 .default
|
|
def name_66 : Lean.Name := .str name_60 "term_+_"
|
|
def expr_270 : Lean.Expr := .forallE name_8 expr_269 expr_46 .default
|
|
def expr_271 : Lean.Expr := .forallE name_8 expr_4 expr_270 .default
|
|
def expr_272 : Lean.Expr := .forallE name_8 expr_241 expr_271 .default
|
|
def expr_273 : Lean.Expr := .forallE name_8 expr_0 expr_272 .default
|
|
def expr_274 : Lean.Expr := .const name_13 [level_0, level_1]
|
|
def expr_275 : Lean.Expr := .app expr_274 expr_15
|
|
def expr_276 : Lean.Expr := .app expr_15 expr_1
|
|
def expr_277 : Lean.Expr := .app expr_253 expr_276
|
|
def expr_278 : Lean.Expr := .app expr_263 expr_20
|
|
def expr_279 : Lean.Expr := .app expr_278 expr_15
|
|
def expr_280 : Lean.Expr := .app expr_279 expr_1
|
|
def expr_281 : Lean.Expr := .app expr_277 expr_280
|
|
def expr_282 : Lean.Expr := .lam name_8 expr_63 expr_281 .default
|
|
def expr_283 : Lean.Expr := .app expr_275 expr_282
|
|
def name_67 : Lean.Name := .str name_64 "intro"
|
|
def expr_284 : Lean.Expr := .const name_67 []
|
|
def expr_285 : Lean.Expr := .app expr_14 expr_20
|
|
def expr_286 : Lean.Expr := .app expr_285 expr_1
|
|
def expr_287 : Lean.Expr := .app expr_15 expr_286
|
|
def expr_288 : Lean.Expr := .app expr_284 expr_287
|
|
def expr_289 : Lean.Expr := .app expr_288 expr_249
|
|
def expr_290 : Lean.Expr := .app expr_3 expr_286
|
|
def name_68 : Lean.Name := .str name_63 "intro"
|
|
def expr_291 : Lean.Expr := .const name_68 []
|
|
def expr_292 : Lean.Expr := .app expr_290 expr_291
|
|
def expr_293 : Lean.Expr := .app expr_289 expr_292
|
|
def expr_294 : Lean.Expr := .app expr_293 expr_291
|
|
def expr_295 : Lean.Expr := .lam name_54 expr_15 expr_294 .default
|
|
def expr_296 : Lean.Expr := .app expr_283 expr_295
|
|
def expr_297 : Lean.Expr := .app expr_20 expr_43
|
|
def expr_298 : Lean.Expr := .app expr_253 expr_297
|
|
def expr_299 : Lean.Expr := .app expr_263 expr_40
|
|
def expr_300 : Lean.Expr := .app expr_299 expr_20
|
|
def expr_301 : Lean.Expr := .app expr_300 expr_43
|
|
def expr_302 : Lean.Expr := .app expr_298 expr_301
|
|
def expr_303 : Lean.Expr := .forallE name_54 expr_20 expr_302 .default
|
|
def expr_304 : Lean.Expr := .app expr_23 expr_40
|
|
def expr_305 : Lean.Expr := .app expr_304 expr_3
|
|
def expr_306 : Lean.Expr := .app expr_20 expr_305
|
|
def expr_307 : Lean.Expr := .app expr_284 expr_306
|
|
def expr_308 : Lean.Expr := .app expr_40 expr_37
|
|
def expr_309 : Lean.Expr := .forallE name_54 expr_40 expr_308 .default
|
|
def expr_310 : Lean.Expr := .app expr_253 expr_309
|
|
def expr_311 : Lean.Expr := .app expr_263 expr_85
|
|
def expr_312 : Lean.Expr := .app expr_311 expr_40
|
|
def expr_313 : Lean.Expr := .app expr_312 expr_37
|
|
def expr_314 : Lean.Expr := .forallE name_54 expr_40 expr_313 .default
|
|
def expr_315 : Lean.Expr := .app expr_310 expr_314
|
|
def expr_316 : Lean.Expr := .app expr_307 expr_315
|
|
def expr_317 : Lean.Expr := .app expr_13 expr_305
|
|
def expr_318 : Lean.Expr := .app expr_284 expr_309
|
|
def expr_319 : Lean.Expr := .app expr_318 expr_314
|
|
def expr_320 : Lean.Expr := .proj name_64 0 expr_43
|
|
def expr_321 : Lean.Expr := .lam name_54 expr_40 expr_320 .default
|
|
def expr_322 : Lean.Expr := .app expr_319 expr_321
|
|
def expr_323 : Lean.Expr := .proj name_64 1 expr_43
|
|
def expr_324 : Lean.Expr := .lam name_54 expr_40 expr_323 .default
|
|
def expr_325 : Lean.Expr := .app expr_322 expr_324
|
|
def expr_326 : Lean.Expr := .app expr_317 expr_325
|
|
def expr_327 : Lean.Expr := .app expr_316 expr_326
|
|
def expr_328 : Lean.Expr := .app expr_327 expr_325
|
|
def expr_329 : Lean.Expr := .lam name_54 expr_303 expr_328 .default
|
|
def expr_330 : Lean.Expr := .lam name_54 expr_22 expr_329 .default
|
|
def expr_331 : Lean.Expr := .app expr_296 expr_330
|
|
def expr_332 : Lean.Expr := .app expr_331 expr_3
|
|
def expr_333 : Lean.Expr := .proj name_64 0 expr_332
|
|
def expr_334 : Lean.Expr := .lam name_54 expr_269 expr_333 .default
|
|
def expr_335 : Lean.Expr := .lam name_54 expr_4 expr_334 .default
|
|
def expr_336 : Lean.Expr := .lam name_54 expr_241 expr_335 .default
|
|
def expr_337 : Lean.Expr := .lam name_54 expr_0 expr_336 .default
|
|
def name_69 : Lean.Name := .str name_54 "mp"
|
|
def decl_7 : Lean.Declaration :=
|
|
.defnDecl {
|
|
name := name_69
|
|
levelParams := [name_16]
|
|
type := expr_273
|
|
value := expr_337
|
|
hints := .opaque
|
|
safety := .safe
|
|
all := [name_69]
|
|
}
|
|
def expr_338 : Lean.Expr := .const name_62 [level_3, level_1]
|
|
def expr_339 : Lean.Expr := .app expr_338 expr_15
|
|
def expr_340 : Lean.Expr := .app expr_339 expr_13
|
|
def expr_341 : Lean.Expr := .app expr_340 expr_1
|
|
def expr_342 : Lean.Expr := .forallE name_16 expr_341 expr_267 .default
|
|
def expr_343 : Lean.Expr := .forallE name_16 expr_56 expr_342 .default
|
|
def expr_344 : Lean.Expr := .forallE name_16 expr_343 expr_46 .default
|
|
def expr_345 : Lean.Expr := .forallE name_16 expr_4 expr_344 .default
|
|
def expr_346 : Lean.Expr := .forallE name_16 expr_213 expr_345 .default
|
|
def expr_347 : Lean.Expr := .forallE name_16 expr_0 expr_346 .default
|
|
def expr_348 : Lean.Expr := .const name_13 [level_6, level_1]
|
|
def expr_349 : Lean.Expr := .app expr_348 expr_15
|
|
def expr_350 : Lean.Expr := .const name_61 [level_4, level_6]
|
|
def expr_351 : Lean.Expr := .app expr_350 expr_276
|
|
def expr_352 : Lean.Expr := .app expr_338 expr_20
|
|
def expr_353 : Lean.Expr := .app expr_352 expr_15
|
|
def expr_354 : Lean.Expr := .app expr_353 expr_1
|
|
def expr_355 : Lean.Expr := .app expr_351 expr_354
|
|
def expr_356 : Lean.Expr := .lam name_16 expr_63 expr_355 .default
|
|
def expr_357 : Lean.Expr := .app expr_349 expr_356
|
|
def name_70 : Lean.Name := .str name_61 "mk"
|
|
def expr_358 : Lean.Expr := .const name_70 [level_4, level_6]
|
|
def expr_359 : Lean.Expr := .app expr_358 expr_287
|
|
def expr_360 : Lean.Expr := .app expr_359 expr_222
|
|
def name_71 : Lean.Name := .str name_60 "unit"
|
|
def expr_361 : Lean.Expr := .const name_71 [level_6]
|
|
def expr_362 : Lean.Expr := .app expr_290 expr_361
|
|
def expr_363 : Lean.Expr := .app expr_360 expr_362
|
|
def expr_364 : Lean.Expr := .app expr_363 expr_361
|
|
def expr_365 : Lean.Expr := .lam name_24 expr_15 expr_364 .default
|
|
def expr_366 : Lean.Expr := .app expr_357 expr_365
|
|
def expr_367 : Lean.Expr := .app expr_350 expr_297
|
|
def expr_368 : Lean.Expr := .app expr_338 expr_40
|
|
def expr_369 : Lean.Expr := .app expr_368 expr_20
|
|
def expr_370 : Lean.Expr := .app expr_369 expr_43
|
|
def expr_371 : Lean.Expr := .app expr_367 expr_370
|
|
def expr_372 : Lean.Expr := .forallE name_24 expr_20 expr_371 .default
|
|
def level_10 : Lean.Level := .max level_6 level_6
|
|
def expr_373 : Lean.Expr := .const name_70 [level_5, level_10]
|
|
def expr_374 : Lean.Expr := .app expr_373 expr_306
|
|
def expr_375 : Lean.Expr := .app expr_227 expr_309
|
|
def expr_376 : Lean.Expr := .app expr_338 expr_85
|
|
def expr_377 : Lean.Expr := .app expr_376 expr_40
|
|
def expr_378 : Lean.Expr := .app expr_377 expr_37
|
|
def expr_379 : Lean.Expr := .forallE name_24 expr_40 expr_378 .default
|
|
def expr_380 : Lean.Expr := .app expr_375 expr_379
|
|
def expr_381 : Lean.Expr := .app expr_374 expr_380
|
|
def expr_382 : Lean.Expr := .const name_70 [level_8, level_8]
|
|
def expr_383 : Lean.Expr := .app expr_382 expr_309
|
|
def expr_384 : Lean.Expr := .app expr_383 expr_379
|
|
def expr_385 : Lean.Expr := .proj name_61 0 expr_43
|
|
def expr_386 : Lean.Expr := .lam name_24 expr_40 expr_385 .default
|
|
def expr_387 : Lean.Expr := .app expr_384 expr_386
|
|
def expr_388 : Lean.Expr := .proj name_61 1 expr_43
|
|
def expr_389 : Lean.Expr := .lam name_24 expr_40 expr_388 .default
|
|
def expr_390 : Lean.Expr := .app expr_387 expr_389
|
|
def expr_391 : Lean.Expr := .app expr_317 expr_390
|
|
def expr_392 : Lean.Expr := .app expr_381 expr_391
|
|
def expr_393 : Lean.Expr := .app expr_392 expr_390
|
|
def expr_394 : Lean.Expr := .lam name_24 expr_372 expr_393 .default
|
|
def expr_395 : Lean.Expr := .lam name_24 expr_22 expr_394 .default
|
|
def expr_396 : Lean.Expr := .app expr_366 expr_395
|
|
def expr_397 : Lean.Expr := .app expr_396 expr_3
|
|
def expr_398 : Lean.Expr := .proj name_61 0 expr_397
|
|
def expr_399 : Lean.Expr := .lam name_24 expr_343 expr_398 .default
|
|
def expr_400 : Lean.Expr := .lam name_24 expr_4 expr_399 .default
|
|
def expr_401 : Lean.Expr := .lam name_24 expr_213 expr_400 .default
|
|
def expr_402 : Lean.Expr := .lam name_24 expr_0 expr_401 .default
|
|
def level_11 : Lean.Level := .succ level_5
|
|
def decl_8 : Lean.Declaration :=
|
|
.defnDecl {
|
|
name := `foo42
|
|
levelParams := [name_14, name_24]
|
|
type := expr_347
|
|
value := expr_402
|
|
hints := .opaque
|
|
safety := .safe
|
|
all := [`foo42]
|
|
}
|
|
def expr_403 : Lean.Expr := .app expr_246 expr_246
|
|
def expr_404 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_405 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_406 : Lean.Expr := .const `foo42 [level_0, level_0]
|
|
def expr_407 : Lean.Expr := .app expr_406 expr_126
|
|
def expr_408 : Lean.Expr := .lam name_24 expr_96 expr_15 .default
|
|
def expr_409 : Lean.Expr := .app expr_407 expr_408
|
|
def expr_410 : Lean.Expr := .app expr_409 expr_36
|
|
def expr_411 : Lean.Expr := .const name_24 [level_0]
|
|
def expr_412 : Lean.Expr := .app expr_388 expr_388
|
|
def expr_413 : Lean.Expr := .lam name_24 expr_359 expr_359 .default
|
|
def expr_414 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_415 : Lean.Expr := .proj name_24 12336 expr_301
|
|
def expr_416 : Lean.Expr := .bvar 12336
|
|
def expr_417 : Lean.Expr := .app expr_243 expr_243
|
|
def expr_418 : Lean.Expr := .app expr_214 expr_214
|
|
def expr_419 : Lean.Expr := .lam name_24 expr_185 expr_185 .default
|
|
def expr_420 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_421 : Lean.Expr := .app expr_127 expr_127
|
|
def expr_422 : Lean.Expr := .forallE name_24 expr_98 expr_98 .default
|
|
def expr_423 : Lean.Expr := .lam name_24 expr_69 expr_69 .default
|
|
def expr_424 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_425 : Lean.Expr := .app expr_11 expr_11
|
|
def expr_426 : Lean.Expr := .app expr_408 expr_408
|
|
def expr_427 : Lean.Expr := .bvar 12336
|
|
def expr_428 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_429 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def level_12 : Lean.Level := .succ level_0
|
|
def expr_430 : Lean.Expr := .lam name_24 expr_296 expr_296 .default
|
|
def expr_431 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_432 : Lean.Expr := .app expr_240 expr_240
|
|
def expr_433 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_434 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_435 : Lean.Expr := .app expr_156 expr_156
|
|
def expr_436 : Lean.Expr := .lam name_24 expr_128 expr_128 .default
|
|
def expr_437 : Lean.Expr := .lam name_24 expr_100 expr_100 .default
|
|
def expr_438 : Lean.Expr := .app expr_72 expr_72
|
|
def expr_439 : Lean.Expr := .app expr_44 expr_44
|
|
def expr_440 : Lean.Expr := .lit (.natVal (decodeNatLit [0]))
|
|
def expr_441 : Lean.Expr := .lam name_24 expr_429 expr_429 .default
|
|
def expr_442 : Lean.Expr := .app expr_410 expr_402
|
|
def expr_443 : Lean.Expr := .lam name_24 expr_375 expr_442 .default
|
|
def expr_444 : Lean.Expr := .lit (.natVal (decodeNatLit []))
|
|
def decl_9 : Lean.Declaration :=
|
|
.thmDecl {
|
|
name := name_24
|
|
levelParams := []
|
|
type := expr_443
|
|
value := expr_0
|
|
}
|
|
|
|
open Lean
|
|
|
|
-- We avoid `Lean.addDecl` as it may be doing additional checks that hide the expected error.
|
|
run_meta do
|
|
for decl in [decl_0, decl_1, decl_2, decl_3, decl_4, decl_5, decl_6, decl_7, decl_8] do
|
|
setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl none)
|
|
|
|
/-- error: (kernel) constant has already been declared '«term_+_»' -/
|
|
#guard_msgs in
|
|
run_meta
|
|
setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl_9 none)
|