后来想想，其实

add (Succ m) Zero
  = add m (Succ Zero)  

因为两个参数都修改了所以不能只考虑第二个参数是 Zero 的情况，到不如再抽一下成

add Zero n = n

add (Succ m) n
  = add m (Succ n)

其实它就是说
- add 0 n = n
- add m n = add (m - 1) (n + 1)

最终的『基线』其实就是 m = 0，然后每一层递归都把 m 减去一（匹配掉一个 Succ，也即『取前驱元 predecessor』） n 加上 1（取后继元），最终就是『往 n 上加 m 次 1』，就实现了加法的语义

这样是不是对于 Coinductive 证明来说就能直接得证了呢？

大佬也来学 Agda 什么的吧（
https://ice1000.org/lagda/MuGenHackingToTheGate.html 这个比较偏向入门级别


顺便问问：大佬的 GitHub 在哪里呢？（其实是想问问之前那个 AST 处理的程序是怎么写的了解一下）
大佬看没看过 GoF 的那些 OO 模式的本本呢？ 🤔
觉得好像看过会更有底气一些，我没看过... 所̶以̶经̶常̶会̶被̶ ̶A̶n̶d̶r̶o̶i̶d̶ ̶的̶开̶发̶者̶们̶吊打̶̶ #Android
觉得好像自己会画图更有底气一些，我没画过多少

其̶实̶我̶很̶想̶吊̶打̶做̶ ̶A̶n̶d̶r̶o̶i̶d̶ ̶开̶发̶的̶，̶可̶是̶不̶了̶解̶ ̶O̶O̶ ̶没̶底̶气̶

#Tools #Linux 删除线生成。

strikeout() { sed 's/\(.\)/\1̶/g' <<<$1 }


zstrikeout() { zenity --entry --text=请复制 --entry-text=`strikeout $1` }

strikeout 'Unicode Strikeout composition test' | xclip

大佬要不要试试入门 ANN（ #CS #PL
魔理沙学姐也写过这种文章

图论和函数式编程也挺好玩的

编译原理是个很实用的内容，我给 GeekAPK 搞的 GeekSpec DSL codegen 就是比较 naive 的一种应用（现在也没有写过自己的 LLVM 编译器，惭愧）
大佬的博客好像没有找到（给个链接？
如果没事的话写点玩转 PostgresSQL 文也可以的 👍

我觉得这个东西还挺好玩的 ，可是有点难... 🤔
尤其是数学我 ****🐔🐒***&%$^$@$

😶 我目前没博客

我去，这么点钱房租够么... #China #Life

.NET 现在这么可怜的么？

我哭了（

哦，大概是 Android 开发现在最吃香，哭哭。

为什么不去开发手游呢

技术就不值一个钱，不如多写几个应用

弄了半天居然是因为这些我手写的代码（而不是由 GeekSpec 定义自动生成的）我疏忽少加了 Nullable notation... 🤔看来我岔开去写 GeekSpec 来生成这些绑定是对的，至少不会写半天又加半天的 ? 记号...

现在看来 Swagger 的规范好正规呢，但是如果 GeekAPk API 要拿 Swagger 重写，那不知道要花多少时间呢

上面提到的 spec，我当时压根没写完，只定义了几个模型

但居然写了 503 行

我的脑子都快 struct 不了这个 YAML 文档了，一大堆二维文法，而且结构又复杂... 🤔
全是竖着的简直淡疼，如果没有 Schema 补齐、可以说 Swagger 这个工具就完全没有用了... （因为写 spec 将花费比现在很多 bootstrap 自动化方案更多的时间...）

  /{username}/token:
    get:
      tags:
        - User
      summary: Authorize user
      operationId: getToken
      parameters:
        - name: password
          in: query
          description: User password
          required: true
          schema:
            type: string
            example: sa1tedFi$h
        - name: username
          in: path
          description: User to get new token
          schema:
            type: string
            example: duangsuse
          required: true
      responses:
        200:
          description: Got app access token
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/AuthToken'
        default:
          description: Auth failed
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'

其实这么复杂的 OpenAPI 3.0 YAML 结构要表示的只是一个最简单最容易理解的定义（指民科的过度设计，但我觉得民科和前端打架还是民科赢 hhhh，实际上都没赢...）：

type datetime: string = Date

result OK: status = 200

data AuthToken "Authorization token"
  = { token: string, expires: datetime }


## Begin API definition

== user

'''
Authorize user
*password: User password
  'example_password'
*username: User to get new token
  'duangsuse'

>OK: Got app access token
>*: Auth failed
'''
getToken(password: string, username-path: string)
  -> (OK) AuthToken
     (*) Error
  = /:username/token

我真的不想去学习『如何阅读几乎全是竖排的 YAML』... 所以想来要 GeekApk 利用 Swagger 好像有点难受（迫真

（好吧，就是迫真自演 GeekSpec，但是，其实我希望能让它可以扩展一下来兼容 Swagger OpenAPI 3.0 YAML，我真的没有说骄傲什么的，比我牛逼的人很多，不缺一个只能写垃圾程序的 duangsuse
以后 GeekSpec 的更新版本或许会能作为 Swagger OpenAPI 的一种描述方式，也能有一个 OpenAPI 的后端

对类型系统了解不够，还停留在 Java 的幼儿园级别...

其实 GeekSpec 还是蛮工程的，所以什么类型系统实际上就没有，不是那种通常 General-Purpose 意义下的类型系统

考虑一下 GeekSpec 类型的用途，就是标记一种数据类型，这种 HTTP 协议其实都有兼容的...（Content-Type，MIME 类型）

比如说 datetime，可能就是说绑定到原生的某种结构对象，和泛型什么的其实根本没关系（当然泛型也不是什么高级玩意）

其实对于 POSIX C 的 time_t 来说，一个所谓的 datetime 或许可以这么表达？

type datetime: string
= (C Linux) time_t
(Ruby) Time

read datetime {
#impl C Linux
return (time_t) atol(str);
#end

#impl Ruby
return Time.at(0, str.to_i, :millisecond)
#end
}

put datetime {
#impl C Linux
size_t size;
char *out;

size = snprinf(out, size, "%l", datetime);
if (size < 0) return NULL;
size++;
out = malloc(size);
if (out == NULL) return NULL;

size = snprintf(out, size, "%l", datetime);

if (size == 0) {
free(out);
return NULL;
}

return out;
#end

#impl Ruby
return sprintf('%i', datetime.tv_sec * 1000 + datetime.tv_usec)
#end
}

validate datetime {
#impl Ruby
str.match? /[0-9]+/
#end
}

路漫漫其修远兮 吾将上下而求索 🤔

#frontend #laravel #PHP https://github.com/mewebstudio/Purifier

HTML 文档标签过滤器

#JavaScript #frontend #Backend https://github.com/sindresorhus/is

对值进行类型检查，很甜、支持 TypeScript 的 Type guard（就是 Kotlin 的智能类型推导）

function excited(arg) {
if (is.string(arg)) {
return arg + '!';
}

if (is.number(arg)) {
return arg & 1926;
}
}

['frog', -1].map(excited).forEach(console.log);

#POstgresql #SQL

#GeekApk https://github.com/duangsuse/GeekApk/commit/ca554b78c042da018366f5138c6799bfe3707522

控制器逻辑的最后一道坎🤔
写完，就开始正式实现控制器逻辑了。

管理员用户验证已经实现了，手工测试正常（但是目前服务器好像不会自动创建第一个管理员用户，是个问题）

用户验证部分，估计一时间考虑的不周全，有些验证应该抽出来单独做的，然后有一个 general 一点的逻辑的可以用 middleware 实现


现在好像越写越没有信心了，大概是垃圾代码写多了（是真的，好多余赘代码、非常平铺直叙或者莫名其妙），时间拖长了（绝望）

我不想重构重构重构... 能用就可以，等待 v2 重写吧（绝望）

有没有愿意帮忙一起实现的（