如何为仅标记export而非public export的函数编写证明？

在Idris里，export仅对外公开函数的类型签名，实现细节仅在定义它的模块内部可见；而public export会同时公开类型和实现。要给foo编写证明，又不想对外泄露foo的实现，可按以下方式操作：

• 在同一模块内编写证明
  模块内部可以直接访问export函数的完整实现，因此无需修改foo的导出标记，直接在同一个文件里编写证明逻辑即可。示例：

  export
  foo : Nat -> Nat
  foo n = n + 1
  
  -- 同模块内的证明
  fooSucc : (n : Nat) -> foo n = S n
  fooSucc n = Refl
  

• 拆分实现与接口（可选）
  若想更清晰地隔离实现和公开接口，可将foo的实现设为private，仅导出函数类型和相关证明。这种方式既能保证内部证明可访问实现，又能严格对外隐藏细节：

  export
  foo : Nat -> Nat
  
  private
  fooImpl : Nat -> Nat
  fooImpl n = n + 1
  
  foo = fooImpl
  
  export
  fooSucc : (n : Nat) -> foo n = S n
  fooSucc n = Refl
  

• 临时改为public export（仅调试用）
  如果只是为了快速编写和验证证明，可临时将export替换为public export，完成证明后再改回export。但这种方式有泄露实现的风险，不适合长期保留。

内容的提问来源于stack exchange，提问作者joel