豆腐脑不是豆腐花:伞哥都自己接指令集了，有打算试将 hol 定理证明器前段语言生成 llvm ir 中间语言吗，这样就可以用 llvm 后端的工具链了，不知道是不是可以减少些工作量。