语法

true       True (unit type)
false      False (empty type)
a -> b     Exponential/function pointer/inference rule
b^a        Exponential/function pointer/inference rule
a => b     Imply (lambda/closure)
a & b      And (struct type)
a | b      Or (enum type)
!a         Not (sugar for `a => false`)
a == b     Equal (sugar for `(a => b) & (b => a)`)
a =^= b    Pow equal (sugar for `b^a & a^b`)
excm(a)    Excluded middle (sugar for `a | !a`)
sd(a, b)   Symbolic distinction (see section [Symbolic distinction])
~a         Path semantical qubit (see section [Path Semantics])
a ~~ b     Path semantical quality (see section [Path Semantics])
(a, b)     Ordered pair (see section [Avatar Logic])
(a : b)    Type judgement (see section [Type judgement])
(f . g)    Function composition
all(a)     Lifts `a` to matching all types
□a         Necessary `a` (modal logic)
◇a         Possibly `a` (modal logic)
foo'       Symbol `foo` (see section [Symbols])
foo'(a)    Apply symbol `foo` to `a`
sym(f, f') Symbolic block (see section [Symbolic blocks])
sym a      Locally declared symbol `a` (see section [Symbolic blocks])

x : a      Premise/argument
let y      Theorem/variable

return x                    Make a conclusion (safe)
unsafe return x             Override safety (unsafe)

sym foo;                    Declare a symbol `foo'`.
axiom foo : a               Introduce axiom `foo` of type `a`
() : a                      Prove `a`, e.g. `() : true`
f(x)                        Apply one argument `x` to `f`
f(x, y, ...)                Apply multiple arguments
match x : a                 If `x : false`
match x (l, r) : c          If `x : (a | b)`, `l : a => c` and `r : b => c`
use <tactic>                Imports tactic
fn <name> : a -> b { ... }  Function
lam <name> : a => b { ... } Lambda/closure

^运算符的优先级高，而->运算符的优先级低。

例如，b^a => b 被解析为 (b^a) => b。 b -> a => b 被解析为 b -> (a => b)。

术语和类型设计

在Hooo中，设计基于一个原则：使术语简单，而使类型复杂。这是因为术语主要用作策略，而类型是想要证明的陈述。

这一原则的哲学是，用户希望专注于要证明什么，而不是如何证明。因此，如何证明应该易于记住，同时有一个清晰的进度概述。

类型总是列在右侧，以便于阅读证明

let <name> = <term> : <type>;

Hooo的设计针对三个用例进行了优化

1. 类型检查性能
2. 证明可读性
3. 源代码维护

这导致了一些设计决策，从正常编程的角度来看可能有些奇怪。

用户被迫根据Hooo的语法显式地执行每个步骤

let y = foo(x) : a;         // Allowed
let y = foo(bar(z)) : a;    // Disallowed

这是因为，否则，用户可能会倾向于将证明压缩成难以阅读的形式。在Hooo中编写证明是对未来的投资。抱怨证明长度的人通常在评估证明系统时采取了错误的方法。

难以阅读的证明在长期内的成本超过了可压缩代码的短期好处。然而，Hooo并不阻止人们努力缩短证明。由于Hooo支持元定理证明，它鼓励用户重用通用定理。这是生成形式化证明的正确方式。

类型判断

大多数现代定理证明助手都是基于依赖类型。依赖类型语言中的一种常见设计是在底层语言之上构建高级语言。这确保了更复杂的高级语言的正确性，只要转换为底层语言的变换是有效的。

技术上，Hooo不是依赖类型。Hooo实际上是简单类型，因为在HOOO EP中，每个类型都是一个命题。然而，由于HOOO EP引入了指数命题，Hooo的强大功能与依赖类型系统相当。

可以认为这是没有标准库的Hooo类似于构建高级语言的底层语言。

例如，而不是

z' : nat'

Hooo需要一个额外的术语来表示类型判断

x : (z' : nat')

直觉是Hooo通过其类型从低到高启动。最低级别的术语非常简单且受限。一旦你为你的需求开发了一个库，Hooo就接近了高级语言。

这种设计的好处是，Hooo可以不断地从低到高启动。可以从现有规则生成新规则，同时保持一组简单的基本术语。

安全性启发式方法

安全性启发式方法用于覆盖两种情况

1. 当证明某事可能导致不一致性时
2. 当用户可能有意证明其他事情时

当尝试证明 all(..) 或 sym(..)(..) 时，安全启发式规则会被触发。这在正常的定理证明中是不寻常的，并且是被劝阻的。例如，如果用户正在设计这种形式的公理，那么最好格外小心，因为它很容易导致无意中的荒谬。

当求解器的安全启发式规则过于强烈时，会使用 unsafe return 语法。这是用户传达这部分需要关注的一种方式。

不安全返回的一个应用场景是需要对不合理的推理进行推理。由于 Hooo 用来检查其他数学语言，有时不仅需要能够对做得正确的案例进行推理，还需要对出错的情况进行推理。当正确使用时，Hooo 可以通过在精心设计的公理后面保护不合理推理来安全地完成。

符号

Hooo 的当前版本使用简单的符号。这意味着，而不是声明数据结构，可以简单地使用例如 foo'(a, b)。符号在使用前必须声明一次。

sym foo;

在其他地方，必须使用符号

use foo;

符号是全局的，所以 foo' 在任何地方都是 foo'。

符号块

由于 Hooo 通过提升 all(..) 表达式中的所有变量来使用隐式量化，它需要一个方法来“冻结”变量以表达某些陈述。

例如，all(a & b -> a) 将 a & b -> a 提升到所有类型 a 和 b。这对于可证明的陈述来说是可以的，但如果存在一个假设 a -> b，则这是不安全的。一个假设 a -> b 是荒谬的。

fn sym_all_pow_absurd : all(a -> b) -> false {
    x : all(a -> b);
    let x2 = x() : a -> b;
    let x3 = x() : (a -> b) -> false;
    let r = x3(x2) : false;
    return r;
}

fn sym_absurd : a & sym(a, all(a' -> b))(a) -> false {
    x : a;
    y : sym(a, all(a' -> b))(a);
    let y2 = y() : a -> false;
    let r = y2(x) : false;
    return r;
}

sym_transport : sym(a, b) & (b == c)^(sym a) -> sym(a, c)

fn sym_eq_refl : sym a  ->  a' == a' {
    sym a;
    use eq_refl;
    use triv;
    let r = triv(eq_refl) : a' == a';
    return r;
}

a == b  ->  f(a) == f(b)

(a == b)^true -> f(a) == f(b)

fn cong_sym_id : true -> cong'(sym(a, a')) {
    use cong_from;
    use refl;

    x : true;

    let x2 = refl() : all(a == b -> a == b);
    let x3 = x2() : all(a == b -> sym(a, a')(a) == sym(a, a')(b));
    let x4 = x3() : sym(f, all(a == b -> f'(a) == f'(b)))(sym(a, a'));
    let r = cong_from(x4) : cong'(sym(a, a'));
    return r;
}

len(concat(a, b)) <=> add(len(a), len(b))

concat[len] <=> add

concat[len][even] <=> add[even]
concat[len][even] <=> eqb
concat[even . len] <=> eqb

ps_core : (a ~~ b) & (a : c) & (b : d) -> (c ~~ d)

q_lift : sd(a, b) & (a == b) -> a ~~ b

ava_univ : !~b & (a, b) & (b : c)  ->  c(a) == b
ava_ava : (a, b(c)) & (b(c) : d)  ->  d(a) => b(c)

ava_collide :
  (b, q1(a1)) & (b, q2(a2)) &
  (q1(a1) : p) & (q2(a2) : p) -> !sd(q1, q2)

sym foo;
sym bar;
sym p;

fn test :
    (b, foo'(a1)) & (b, bar'(a2)) &
    (foo'(a1) : p') & (bar'(a2) : p')
-> false {
    arg : (b, foo'(a1)) & (b, bar'(a2)) &
          (foo'(a1) : p') & (bar'(a2) : p');
    use std::ava_collide;
    let x = ava_collide(arg) : !sd(foo', bar');
    let y = () : sd(foo', bar');
    let r = x(y) : false;
    return r;
}

ava_lower_univ : !~p & (b, a) & (a : p) -> p(b) == a