Jackie Shen
Jackie Shen
添加匿名函数
就是我在证明 specific fact时候，我也把 涉及到的符号替换成 数值 去试一试。所以 a> 0 我先证明 a > 0 不行，然后再 1 > 0 ，行，也能证明
``` # eval_fn 在返回的时候，会检查 fn f(n Z) know forall n Z: n % 3 = 1 => f(n) = n know forall n Z: n % 3 = 2 =>...
如何在litex里计算： 1. 只要有 if-else, for 就能计算了 2. for 对应数学归纳 3. if-else对应 litex 的 prove_in_each_case 和 or 4. 数学里没有变量，litex 的 eval 里也没有
``` # sequence and finite sequence is defined in kernel_litex_code/kernel_litex_code.go fn_template seq(s set): fn (n N_pos) s fn_template finite_seq(s set, n N_pos): fn (x N_pos) s: dom: x
# Set the symbol with a value claim: forall s, s2 set: s := {x R: 1 : s = s2 # 根据 s >= s2, s