关于：`projNonPropFromProp`🔗

Error code: lean.projNonPropFromProp

Tried to project data from a proof.

Severity: ErrorSince: 4.23.0

当尝试使用索引投影从命题证明中投影数据时，会产生此错误。例如，如果 h 是存在性命题的证明，尝试提取见证 h.1 就是此错误的一个例子。不允许此类投影，因为它们可能违反 Lean 禁止从 Prop 进行大消去的规定（详见手册中的命题一节）。

不要使用索引投影，而应考虑使用模式匹配 Lean.Parser.Term.let : termlet、Lean.Parser.Term.match : termmatch 表达式，或 cases 之类的解构策略，将一个命题类型消去到另一个命题类型。注意，只有当结果值也位于 Prop 中时，这种消去才有效；否则将引发错误 lean.propRecLargeElim。

示例🔗

尝试对存在性证明使用索引投影

example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > 0 :=
  ⟨Invalid projection: Cannot project a value of non-propositional type
  Nat
from the expression
  h
which has propositional type
  ∃ x, x > a + 1h.1, Nat.lt_of_succ_lt h.2⟩

Invalid projection: Cannot project a value of non-propositional type
  Nat
from the expression
  h
which has propositional type
  ∃ x, x > a + 1

example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a :=
  let ⟨w, hw⟩ := h
  ⟨w, Nat.lt_of_succ_lt hw⟩

example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a := by
  cases h with
  | intro w hw =>
    exists w
    omega

不能使用索引投影提取存在性命题证明所关联的见证。必须使用模式匹配：可以使用类似 Lean.Parser.Term.let : termlet 的项绑定，或类似 cases 的策略。

关于：projNonPropFromProp🔗

示例🔗

关于：`projNonPropFromProp`🔗