Commits

Branch selector

 main

User selector

All users

Datepicker

All time

Commit History

Commits on Feb 5, 2024

• Separating out the less than part of little o into not le

  calcu16

  committed
  d267eb4

  Copy full SHA for d267eb4

• Closing in on Karatsuba

  calcu16

  committed
  142a3fa

  Copy full SHA for 142a3fa

Commits on Jan 26, 2024

• Lean version of karatsuba

  calcu16

  committed
  02c54c5

  Copy full SHA for 02c54c5

Commits on Jan 23, 2024

• Refactor builds

  calcu16

  committed
  3b728a2

  Copy full SHA for 3b728a2

• Refactoring a bit

  calcu16

  committed
  a279e27

  Copy full SHA for a279e27

Commits on Jan 21, 2024

• builds

  calcu16

  committed
  2d567e4

  Copy full SHA for 2d567e4

• .

  calcu16

  committed
  b179019

  Copy full SHA for b179019

• Nat.add but its ugly

  calcu16

  committed
  4b93bba

  Copy full SHA for 4b93bba

Commits on Jan 20, 2024

• fixing typo and working towards Nat.mul

  calcu16

  committed
  5aaf463

  Copy full SHA for 5aaf463

Commits on Jan 19, 2024

• Starting on Nat

  calcu16

  committed
  9e9aee5

  Copy full SHA for 9e9aee5

• Simple loop complexity - O(n) loops of O(1) work takes O(n) time

  calcu16

  committed
  8f5d1fa

  Copy full SHA for 8f5d1fa

Commits on Jan 16, 2024

• Building

  calcu16

  committed
  9ac7aba

  Copy full SHA for 9ac7aba

Commits on Jan 15, 2024

• Cleaning up a bit

  calcu16

  committed
  fb50006

  Copy full SHA for fb50006

• Changing notation

  calcu16

  committed
  fd69a53

  Copy full SHA for fd69a53

Commits on Jan 14, 2024

• Proof of splitting cost and beginnings of HasCost framework - switching asymptotically less than to be a type to remain computable

  calcu16

  committed
  9435779

  Copy full SHA for 9435779

Commits on Jan 13, 2024

• Finished instance refactor, now takes raw traces

  calcu16

  committed
  93d3001

  Copy full SHA for 93d3001

• Starting to move TracedProgram building into inferred instance

  calcu16

  committed
  83b5fbc

  Copy full SHA for 83b5fbc

• Refactoring Option.Forall/Option.Exists

  calcu16

  committed
  3f513a0

  Copy full SHA for 3f513a0

Commits on Jan 11, 2024

• Working towards asymptotic complexity

  calcu16

  committed
  f489987

  Copy full SHA for f489987

Commits on Jan 5, 2024

• Minor changes

  calcu16

  committed
  b1df62d

  Copy full SHA for b1df62d

• Starting asymptotics

  calcu16

  committed
  adaf245

  Copy full SHA for adaf245

• Removing old trace

  calcu16

  committed
  2e7e4bc

  Copy full SHA for 2e7e4bc

• Moving to new trace

  calcu16

  committed
  1a3ff14

  Copy full SHA for 1a3ff14

Commits on Jan 4, 2024

• Combining Trace and Program into a single entity, and forcing a decode function on Encodings

  calcu16

  committed
  e93a373

  Copy full SHA for e93a373

Commits on Jan 3, 2024

• Starting on TracedProgram

  calcu16

  committed
  ea9395c

  Copy full SHA for ea9395c

Commits on Jan 2, 2024

• f

  calcu16

  committed
  08db78f

  Copy full SHA for 08db78f

Commits on Jan 1, 2024

• Starting asymptotics

  calcu16

  committed
  109ce46

  Copy full SHA for 109ce46

Commits on Dec 31, 2023

• Switching to using a Nat height instead of ACC for wellfounded

  calcu16

  committed
  f6001f6

  Copy full SHA for f6001f6

• Everything except proving wellFounded in recursive functions

  calcu16

  committed
  1c34273

  Copy full SHA for 1c34273

• [simp] Up through wellFounded recursion

  calcu16

  committed
  347da6c

  Copy full SHA for 347da6c

Commits on Dec 29, 2023

• wip2

  calcu16

  committed
  4e75a34

  Copy full SHA for 4e75a34

• wip

  calcu16

  committed
  835055e

  Copy full SHA for 835055e

Commits on Dec 25, 2023

• Adding .lake to gitignore

  calcu16

  committed
  13d06e7

  Copy full SHA for 13d06e7

• Upgrading mathlib/lean4

  calcu16

  committed
  d05db05

  Copy full SHA for d05db05

Commits on Dec 24, 2023

• Missing files

  calcu16

  committed
  8ec1742

  Copy full SHA for 8ec1742

Pagination

Previous

Next