Commits

Branch selector

 main

User selector

All users

Datepicker

All time

Commit History

Commits on Nov 14, 2021

• Chapter 3 in progress

  mk12

  committed
  e85deae

Commits on May 3, 2020

• Update README and Coq Makefile

  mk12

  committed
  8e35a10

Commits on Dec 30, 2018

• Done Chapter2 in Coq

  mk12

  committed
  099e17a

• Progress

  mk12

  committed
  097a262

Commits on Dec 28, 2018

• Done mul_comm

  mk12

  committed
  35c9419

• Ready for multiplication

  mk12

  committed
  4bc9404

• Done strong induction

  mk12

  committed
  1af0e05

• Done ordering stuff

  mk12

  committed
  5c64379

Commits on Dec 27, 2018

• More progress

  mk12

  committed
  63b99d2

• Using 'now'

  mk12

  committed
  f4d954b

• Finished up to trichotomy

  mk12

  committed
  aba0012

Commits on Dec 26, 2018

• Improving for coqdoc

  mk12

  committed
  0a0bf43

• Checkpoint

  mk12

  committed
  e1266f8

• Progress

  mk12

  committed
  1f60954

Commits on Dec 25, 2018

• Custom coq beautifier

  mk12

  committed
  2b66fb0

• More progress

  mk12

  committed
  814aa15

• Start the Coq rewrite

  mk12

  committed
  088d0d3

• Move lean stuff in its own folder

  mk12

  committed
  7490873

Commits on Aug 3, 2017

• Start converting Mem, Fun, ... to Lean3

  mk12

  committed
  598a5dc

• Convert more theorems to Lean3

  mk12

  committed
  f9a1682

Commits on Aug 2, 2017

• Ported a few more sections of chapter 3 to Lean3

  mk12

  committed
  6e763d0

Commits on Jul 29, 2017

• More progress porting chapter 3

  mk12

  committed
  87d2fd5

• Starting to port chapter 3 to Lean 3

  mk12

  committed
  71fe2ea

Commits on Jul 27, 2017

• Start porting chapter 3

  mk12

  committed
  0b10f3c

• Use by_cases instead of cases_on (lots of this isn't constructive anyway)

  mk12

  committed
  3eaff8d

• Fix some things

  mk12

  committed
  385be04

• Finished porting chapter_2.lean to Lean 3!

  mk12

  committed
  de7a619

Commits on Jul 26, 2017

• More progress

  mk12

  committed
  666a137

• Port strong induction

  mk12

  committed
  e5f601d

• Use .mp and .mpr for iffs

  mk12

  committed
  8c43288

• Rename zero_ne_succ to succ_ne_zero (reflect actual arg order)

  mk12

  committed
  86891a7

• Prove add_eq_zero constructively

  mk12

  committed
  7aef177

• More progress in porting to Lean3

  mk12

  committed
  8b44e61

Commits on Jul 25, 2017

• More progress

  mk12

  committed
  ac2f694

Commits on Jul 24, 2017

• Port a few more propositions

  mk12

  committed
  c7563d4

Pagination

PreviousNext