Well-founded Recursion
Generalizing structural recursion for languages with termination checker, part 1
Learning note of Ltac2
Organizing what's in the official documentation
Inductive type and W Type
Generalizing inductive types
Lens - Exploring and Learning - 1
Introduction / Abstractions of "setter"s and "getter"s.
Adjoint Functor
Notes on the category theory concept.
C++ Higher-order Meta-function
Some simple template tricks
Agda Learning Note
Notes on agda core language and standard library.
Bash Notes
Notes on the bash language
My C++ Style Guide
My C++ coding style mostly based on Google C++ Style Guide
Leetcode Solution Collection
Homework for algorithm course in SYSU
Haskell Monad Basic - 5
Monad Transformer
Haskell Monad Basic - 4
Reader, Writer and State
Haskell Monad Basic - 3
Monad and its "super classes"
Haskell Monad Basic - 2
value and context, basic examples on List, Maybe and Either
Haskell Monad Basic - 1
motivation, introduction, definition of Monad and the "do" notation
Hello World
hello, my blog