主要观点：PeanoScript 是基于 TypeScript 语法的 Peano 算术证明助手，旨在让程序员易于使用，能正式证明数学命题、将证明作为程序运行、理解构造逻辑与经典逻辑的区别及理解相关类型。介绍了 Peano 算术的公理、自然数、算术表达式、等式、函数、全称量词、存在量词等概念及相关操作，还提到了一些逻辑连接词如“与”“或”等，以及如何使用ring内置函数进行等式变换等。

关键信息：

• Peano 算术公理包括后继非零、后继单射、加法零、加法后继、乘法零、乘法后继、归纳模式等。
• 基本对象是自然数，可通过const variableName = number;赋值，变量有类型且通常可推断。
• 算术表达式可进行加乘运算，运算符有优先级。
• 等式用a == b表示，可通过eqRefl(x)获取自反性证明，等式有对称、传递等性质。
• 函数用箭头/ lambda 记法表示，类型可通过(_: A) => B指定，可使用sorry表示暂未完成的证明。
• 全称量词用“∀”表示，存在量词用“∃”表示，存在量词类型类似依赖对类型。
• 逻辑连接词“与”用“&&”表示，“或”用“||”表示，可使用match语句处理。
• 可使用ring函数进行等式变换，never表示逻辑矛盾。

重要细节：

• PeanoScript 基于 TypeScript 语法，如变量类型推断等。
• 各种逻辑概念和操作在代码中的具体实现方式，如证明各种性质的函数和表达式。
• 不同类型的函数和量词在代码中的表示形式及使用方法，如单参数函数、多参数函数、依赖函数等。
• 各种逻辑连接词在代码中的应用场景和语法，如&&和||的使用及match语句的结构。
• replace函数用于根据等式替换公式中的变量等操作。