Zero Calorie Drink Shop

A childless azukisan lady who is miserable at her own live.

That is me. Only a nihilistic phantom.

[Feed] [GitHub]

试试 idris2

唉早知道就不折腾这种全世界都找不出一万个人在用的东西了.txt

vite-plugin-vue-layouts 使用记

前言: unplugin-vue-router 是 unplugin 的一款插件,旨在在 src/pages 等目录下使用文件驱动的 routing 来避免手写 vue-router 配置带来的麻烦与潜在的失误,是约定优于配置的一个展现。

vite-plugin-vue-layouts 是与 unplugin-vue-router 非常般配的一款插件,旨在为 views 指定共享的 layout,在复杂前端工程上或许非常有用。

二者是 vuetify 前端框架推荐使用的插件。

然后就被它的【刻意的设计】坑了一把

PFPL 笔记 - VI Dynamic Types

笔记 7

学习在 Lean4 中使用 Parser Combinator

此时对于我那幽默的《编译原理》课程还在用 C 语言写编译器的不满达到了顶峰。

你说得对,但是《编译原理》是由 Alfred V. Aho, Monica S. Lam, Ravi Sethi 和 Jeffrey D. Ullman 等人自主研发的一款全旧计算机世界编程游戏。游戏发生在一个被称作「C–」的简化语言,在这里,选择这门课的人将被迫享受「GCC 7.5.0」,没有一点 5202 年该有的体验。玩家将扮演一位名为「C 程序员」的神秘角色,在自由的编码中邂逅各种各样、时机诡异的 Segment Fault 们,和他们一起泄露内存,感受 C 语言的恶心之处——同时,逐步发掘「都 5202 年了这帮人还在拿 39 年前的书教文法分析」的真相。

但跑远了。总而言之这里介绍一种叫 parser combinator —— 解析器组合子的函数式手段,为您带来哪怕是手写递归下降也很舒适的体验(并非)

很难不承认 Lean4 真香 —— 然后写了一个简单的 JSON 解析器

在之前的文章中我尝试了一下 Lean4 定理证明器——然后我是在并非干这个方向的所以后面就抛在脑后了

后面因为学习函数式语言于是又捡起了 Lean4 函数式编程,然后……好吧我真的不得不说真香啊

一千个计算机人有一千个强类型

所以不要再说强类型了啊!!

小数据的时候 `std::vector<int>` 删除首元素比 deque 和 list 还快

链表可以当成双端队列来使用——至少在渐进时空复杂度上,它们是相同的。

但在现代化的 CPU 的支持下,std::vector 由于内存的连贯性,在小规模数据下甚至可以做到比 std::deque 更好的性能,更别提在随机访问上 std::vector 有巨大优势了。

所以这个 Monads 到底是什么啊之让我学学

简单的说单子(Monad)就是自函子范畴上的一个幺半群 👀 你说这个谁懂啊

PFPL 笔记 - VI Dynamic Types

笔记 6
最详细的一集,因为我要讲解这部分(摊手
但是读得很开心!这章真是让我受益匪浅啊!

PFPL 笔记 - V Infinite Data Types

笔记5

Next