Commits

Branch selector

main

User selector

All users

All time

Commit history

Commits on Jul 31, 2026

• Update toolchain and remove direct mathlib dependency (#73)

  Show description for c33724e
  Shreyas4991

  authored
  c33724eView commit details

  Copy full SHA for c33724e

  Browse repository at this point

Commits on Jul 26, 2026

• remove needless comment

  arademaker

  committed
  8171bdcView commit details

  Copy full SHA for 8171bdc

  Browse repository at this point

• Merge branch 'ex-48-fixed'

  arademaker

  committed
  39b7109View commit details

  Copy full SHA for 39b7109

  Browse repository at this point

• Exercise 4.8 - changed example to theorem

  arademaker

  committed
  c79ad78View commit details

  Copy full SHA for c79ad78

  Browse repository at this point

Commits on Jul 25, 2026

• Merge branch 'ex-41-fixed'

  arademaker

  committed
  f2e85c9View commit details

  Copy full SHA for f2e85c9

  Browse repository at this point

• refactor(chapter3): drop splitInTwoSL from simp

  Show description for 6f0548f
  arademaker

  committed
  6f0548fView commit details

  Copy full SHA for 6f0548f

  Browse repository at this point

• refactor(chapter4): rework Ex 4.1 to follow the statement faithfully

  Show description for 7461405
  arademaker

  committed
  7461405View commit details

  Copy full SHA for 7461405

  Browse repository at this point

Commits on Jul 23, 2026

• Exercise 4.8 solved

  GabrielJP314

  authored
  48d25c0View commit details

  Copy full SHA for 48d25c0

  Browse repository at this point

• Exercise 4.1 solved

  GabrielJP314

  authored
  8bfdc0dView commit details

  Copy full SHA for 8bfdc0d

  Browse repository at this point

• refactor(chapter3): RAList namespace

  Show description for 62edb98
  arademaker

  committed
  62edb98View commit details

  Copy full SHA for 62edb98

  Browse repository at this point

• review changes

  arademaker

  committed
  5de8200View commit details

  Copy full SHA for 5de8200

  Browse repository at this point

Commits on Jul 21, 2026

• Exercise 3.10 solved (#66)

  Show description for b39ef23
  GabrielJP314

  authored
  b39ef23View commit details

  Copy full SHA for b39ef23

  Browse repository at this point

• chapter3: fix order of definitions

  arademaker

  committed
  9dc028eView commit details

  Copy full SHA for 9dc028e

  Browse repository at this point

Commits on Jul 10, 2026

• docs(chapter1): document foldl fusion law in Exercise 1.18

  Show description for 76c6215
  arademaker

  committed
  76c6215View commit details

  Copy full SHA for 76c6215

  Browse repository at this point

Commits on Jul 9, 2026

• refactor(chapter1): simplify Exercise 1.17 fusion proofs

  Show description for 2ff8e34
  arademaker

  committed
  2ff8e34View commit details

  Copy full SHA for 2ff8e34

  Browse repository at this point

• Exercise 1.17 solved (#65)

  Show description for 858ad94
  GabrielJP314

  authored
  858ad94View commit details

  Copy full SHA for 858ad94

  Browse repository at this point

Commits on Jul 8, 2026

• feat(chapter3): prove dropWhileSL, initsSL and inits₁ = inits₂

  Show description for 318fe8c
  arademaker

  committed
  318fe8cView commit details

  Copy full SHA for 318fe8c

  Browse repository at this point

Commits on Jul 7, 2026

• feat(chapter3): prove SymList lemmas and refactor concat time bounds

  Show description for 5fbfd56
  arademaker

  committed
  5fbfd56View commit details

  Copy full SHA for 5fbfd56

  Browse repository at this point

Commits on Jun 23, 2026

• feat(chapter2): add TimeM complexity proofs for concat₁ and concat₂

  Show description for a88e775
  arademaker

  committed
  a88e775View commit details

  Copy full SHA for a88e775

  Browse repository at this point

Commits on Jun 16, 2026

• chore: remove assignment files and simplify termination proofs

  Show description for 8013e71
  arademaker

  committed
  8013e71View commit details

  Copy full SHA for 8013e71

  Browse repository at this point

Commits on Jun 15, 2026

• fix(chapter1): simplify proofs and move inits/tails to Chapter1-Ex

  Show description for 1aa4bca
  arademaker

  committed
  1aa4bcaView commit details

  Copy full SHA for 1aa4bca

  Browse repository at this point

• feat(chapter1): add termination proofs and collapse equivalence

  Show description for 00d328b
  arademaker

  committed
  00d328bView commit details

  Copy full SHA for 00d328b

  Browse repository at this point

Commits on Jun 11, 2026

• fix: solve perms1 and perms2 in chapter1

  arademaker

  committed
  251e886View commit details

  Copy full SHA for 251e886

  Browse repository at this point

Commits on Dec 17, 2025

• chore: upgrade to Lean v4.27.0-rc1

  Show description for ac40e4f
  arademaker

  committed
  ac40e4fView commit details

  Copy full SHA for ac40e4f

  Browse repository at this point

Commits on Dec 10, 2025

• fix: minor syntax adjustment

  arademaker

  committed
  5412315View commit details

  Copy full SHA for 5412315

  Browse repository at this point

• fix: minor syntax adjustment

  arademaker

  committed
  ca63193View commit details

  Copy full SHA for ca63193

  Browse repository at this point

• fix(chapter4): complete flatten proof (#62)

  Show description for 41c9a7f
  m-ow

  authored
  41c9a7fView commit details

  Copy full SHA for 41c9a7f

  Browse repository at this point

• feat(chapter5): prove reverse equivalence (#64)

  Show description for ff77a3c
  m-ow

  authored
  ff77a3cView commit details

  Copy full SHA for ff77a3c

  Browse repository at this point

Commits on Dec 3, 2025

• fix(chapter1): complete scanr proof in Ex 1.12.

  Show description for bd75856
  m-ow

  authored
  bd75856View commit details

  Copy full SHA for bd75856

  Browse repository at this point

• test(chapter3): improve fetch function examples

  Show description for 4e8542f
  arademaker

  committed
  4e8542fView commit details

  Copy full SHA for 4e8542f

  Browse repository at this point

Commits on Nov 14, 2025

• fix README

  arademaker

  committed
  b9905eeView commit details

  Copy full SHA for b9905ee

  Browse repository at this point

• update README

  arademaker

  committed
  2227ecdView commit details

  Copy full SHA for 2227ecd

  Browse repository at this point

Commits on Nov 13, 2025

• fix : lakefile.toml default target

  arademaker

  committed
  0e87086View commit details

  Copy full SHA for 0e87086

  Browse repository at this point

• update workflow

  arademaker

  committed
  b59d4c8View commit details

  Copy full SHA for b59d4c8

  Browse repository at this point

• update worflow and README flag

  arademaker

  committed
  4e9f4b2View commit details

  Copy full SHA for 4e9f4b2

  Browse repository at this point