🌐 Theorems that rule this multiverse
Switch branches/tags
Nothing to show
Clone or download
Latest commit 7dc0ea4 Oct 6, 2018
Failed to load latest commit information.
.circleci Siji weiwu! Oct 6, 2018
src Refactor some proof Oct 6, 2018
.gitignore update all files Nov 15, 2017
LICENSE Initial commit Nov 11, 2017
README.md use sym instead of providing `xxx-flip` Nov 30, 2017
theorems.agda-lib rename package Nov 11, 2017



CircleCI GitHub top language

Theorems proving codes, written in Agda.

Each proof is put into separate files, except those very very short ones.

This library depends on the Agda standard library.

All Proofs

You can either:

File structure

module Meow where -- module definition

open import Data.Meow -- imports

-- definitions

meow~ : Meow -- some basic function definitions here

-- internal stuffs


  ⌈meow≶meow⌉ : Meow ≡ Meow -- proofs here, with strange but readable naming
                            -- you'll never know how I type those characters

-- public aliases

meow-meow : Meow ≡ Meow
meow-meow = ⌈meow≶meow⌉ -- regulated aliases, using ascii characters