Literate Agda 博客

这是使用 Literate Agda 写的一个博客系列。 由于这种博客的排版和文章组织方式区别非常大,因此单独放在一起。

{-# OPTIONS --no-unicode  #-}
{-# OPTIONS --without-K   #-}
{-# OPTIONS --no-main     #-}
{-# OPTIONS --cubical     #-}
{-# OPTIONS --rewriting   #-}
{-# OPTIONS --copattern   #-}
{-# OPTIONS --sized-types #-}
{-# OPTIONS --prop        #-}

module index where

通过添加很多其实在这个目录页面没有什么用的 Pragma 来呼吁大家关爱 Haskell 程序员。

文章目录

import Typeclassopedia using ()
  -- date: 2018/11/1
  -- 使用 `record` 实现类型类

import DependentFunctionsVersusDynamicTyping using ()
  -- date: 2018/11/7
  -- 形式验证、依赖类型与动态类型

import MuGenHackingToTheGate using ()
  -- date: 2018/11/11
  -- 无限大的大小与余归纳数据结构

import CopatternIsMoreThanCoinduction using ()
  -- date: 2018/11/12
  -- copattern 的其他用处

杂项

import TypesettingTests using ()
  -- date: 2018/11/2
  -- 排版测试