Commit Graph

Select branches

Hide Pull Requests

conor

master

projecteuler-2-progress

tidyup

#1

#100

#101

#102

#103

#104

#105

#106

#107

#108

#109

#110

#111

#112

#113

#114

#115

#116

#117

#118

#119

#120

#121

#122

#123

#124

#125

#126

#127

#128

#129

#130

#131

#15

#16

#17

#18

#19

#2

#20

#21

#22

#23

#24

#25

#26

#27

#28

#3

#30

#31

#32

#33

#34

#35

#36

#37

#39

#4

#40

#41

#42

#43

#44

#45

#46

#47

#48

#49

#5

#50

#51

#52

#53

#54

#55

#56

#57

#58

#59

#60

#61

#62

#63

#64

#65

#66

#67

#68

#69

#70

#71

#72

#73

#74

#75

#76

#77

#78

#79

#80

#81

#82

#83

#85

#86

#87

#88

#89

#90

#91

#92

#93

#94

#95

#97

#98

#99

Mono Color

• 0f42300110 Total order examples (#130) master Patrick Stevens 2021-11-08 23:10:40 +00:00
• 888670b114 Unfinished ordinals stuff and a tiny bit of division (#131) Patrick Stevens 2021-11-08 23:10:25 +00:00
• ada3c189e2 Add GitHub Workflow (#129) Patrick Stevens 2021-11-07 15:12:35 +00:00
• b917beaeaf Add Church numerals Smaug123 2021-11-07 09:48:57 +00:00
• 7f4ed2ec7e Bump up to 2.6.2 Smaug123 2021-10-31 18:19:15 +00:00
• 4b8f6993d0 Tidy up a bit (#127) Patrick Stevens 2020-05-19 07:44:42 +01:00
• df591cc5f9 Tidy a bit tidyup Smaug123 2020-05-19 07:41:29 +01:00
• b57cbb8ea6 Bump Agda (#128) Patrick Stevens 2020-04-26 20:55:05 +01:00
• cb28fd4ab9 Progress projecteuler-2-progress Smaug123 2020-04-25 08:19:33 +01:00
• cab004f6d8 More lecture notes (#126) Patrick Stevens 2020-04-19 20:15:02 +01:00
• 485b27e009 ProjectEuler 2, nearly (#125) Patrick Stevens 2020-04-19 13:40:22 +01:00
• e660eceb43 Hide more stuff (#124) Patrick Stevens 2020-04-19 07:54:37 +01:00
• 3afdc6d45b Actually fix the build (#123) Patrick Stevens 2020-04-19 07:17:23 +01:00
• 750a77b7d8 Fix build (#122) Patrick Stevens 2020-04-18 20:14:58 +01:00
• f8db6a555c Maybe FieldOfFractions.Order slightly faster (#121) Patrick Stevens 2020-04-18 20:08:24 +01:00
• b2333ee455 Tidy up Entails a bit (#111) Patrick Stevens 2020-04-18 20:02:30 +01:00
• adeb398a21 Make more stuff private (#120) Patrick Stevens 2020-04-18 19:56:11 +01:00
• 1831ef49c4 Move Functions (#119) Patrick Stevens 2020-04-18 17:47:27 +01:00
• 84a146f72c Move Bool to live on its own (#118) Patrick Stevens 2020-04-18 17:14:39 +01:00
• 264a5e2bd9 Partially ordered ring, at last (#117) Patrick Stevens 2020-04-16 21:58:35 +01:00
• 9b80058157 Lots of speedups (#116) Patrick Stevens 2020-04-16 13:41:51 +01:00
• 1bcb3f8537 Irrelevant field of fractions (#115) Patrick Stevens 2020-04-13 14:09:23 +01:00
• 46fcb023d4 Base expansions do approximate the number (#114) Patrick Stevens 2020-04-13 11:43:35 +01:00
• 269f2aa14f N-ary expansions (#113) Patrick Stevens 2020-04-12 12:16:20 +01:00
• 380548134d Move towards base-n expansions (#112) Patrick Stevens 2020-04-11 19:46:26 +01:00
• e9aa1bcc05 Lots of without-K (#110) Patrick Stevens 2020-04-11 12:14:03 +01:00
• 412edaf4c7 Lots of refactoring towards partially-ordered ring R (#109) Patrick Stevens 2020-04-10 19:00:57 +01:00
• 1cff95c652 UFD progress (#108) Patrick Stevens 2020-04-10 09:24:53 +01:00
• f5bac0c091 Move the tautology stuff (#107) Patrick Stevens 2020-04-05 19:27:59 +01:00
• 2f07a8e972 Free-group lemmas (#106) Patrick Stevens 2020-04-05 11:09:12 +01:00
• 61b5f8acc5 Universal property of free product (#105) Patrick Stevens 2020-03-29 12:44:50 +01:00
• a27375db4e Define the free product (#104) Patrick Stevens 2020-03-28 21:34:14 +00:00
• 162a1c7a40 Termination checker got a bit sad on upgrade to Agda 2.6.1 (#103) Patrick Stevens 2020-03-28 18:10:55 +00:00
• d2d1c4d3f2 Free group universal property (#102) Patrick Stevens 2020-03-22 13:08:10 +00:00
• e0e627514e Tweak tautology (#100) Patrick Stevens 2020-02-23 12:35:05 +00:00
• f6b13d677a Fix up the classical five to avoid duplicated work (#101) Patrick Stevens 2020-02-23 12:16:19 +00:00
• 29216d26cb Met and Top lecture 1 (#99) Patrick Stevens 2020-02-23 12:12:53 +00:00
• f41f5226b9 Some graphs stuff (#98) Patrick Stevens 2020-02-15 13:41:51 +00:00
• 9de323c5e8 Alternative LUB property (#97) Patrick Stevens 2020-02-13 07:51:41 +00:00
• d183b40d11 Definitions for the reals, classically (#95) Patrick Stevens 2020-02-08 13:20:21 +00:00
• d29c7ea681 Some basic sets (#94) Patrick Stevens 2020-02-03 07:09:51 +00:00
• cbe55c9b56 Rem unused opens in Safe (#93) Patrick Stevens 2020-01-05 15:06:35 +00:00
• 019a9d9a07 Cleanup finset and modulo (#92) Patrick Stevens 2020-01-01 10:14:55 +00:00
• b6ef9b46f2 Reshuffle orders (#91) Patrick Stevens 2019-12-29 12:11:21 +00:00
• 876396eaaa Another phrasing of Euclidean Domain (#90) Patrick Stevens 2019-12-23 10:26:20 +00:00
• 2f64111407 List is a monad (#89) Patrick Stevens 2019-12-08 12:11:49 +00:00
• 33098e94b0 Progress towards UFDs (#88) Patrick Stevens 2019-12-08 11:18:39 +00:00
• 99c38495ce Irreducible and maximal (#87) Patrick Stevens 2019-12-07 18:53:08 +00:00
• e192f0e1f1 Z is a Euclidean domain (#86) Patrick Stevens 2019-12-07 13:00:18 +00:00
• cfd9787bb8 Problem 1 of Project Euler (#85) Patrick Stevens 2019-12-04 19:53:34 +00:00
• 2ed7bd8044 More rings stuff (#83) Patrick Stevens 2019-11-23 13:53:54 +00:00
• 660d7aa27c Lots of rings (#82) Patrick Stevens 2019-11-22 19:52:57 +00:00
• b33baa5fb7 Quotient ring (#81) Patrick Stevens 2019-11-21 07:28:25 +00:00
• d4f51a3efe Restructure towards ideals (#80) Patrick Stevens 2019-11-20 22:00:09 +00:00
• 0078ca9c2d Missed one Smaug123 2019-11-20 21:53:53 +00:00
• b03a5279bc Restructure towards ideals Smaug123 2019-11-20 21:20:03 +00:00
• f2f4e867fc Rejig subgroups, add ideals (#79) Patrick Stevens 2019-11-19 19:56:01 +00:00
• f0790e4f52 Polynomial ring (#78) Patrick Stevens 2019-11-19 08:45:08 +00:00
• 07ffda201a Travis fix (#77) Patrick Stevens 2019-11-17 18:05:19 +00:00
• 8377c23613 Polynomial ring (#76) Patrick Stevens 2019-11-17 17:37:10 +00:00
• c55dd5f63e Reshuffle in preparation to break the dependency on N's implementation (#75) Patrick Stevens 2019-11-17 10:01:39 +00:00
• ff6ef4f1a1 Direct sums: preparing for vector spaces (#74) Patrick Stevens 2019-11-16 15:06:57 +00:00
• 9419587eb0 Modules (as in "vector space but over a ring") (#73) Patrick Stevens 2019-11-16 12:32:40 +00:00
• 46758a1a01 And lemmas Smaug123 2019-11-16 12:26:26 +00:00
• 36858dcbb2 Modules into Everything Smaug123 2019-11-16 12:19:29 +00:00
• f8a2062c6e Modules Smaug123 2019-11-16 12:18:03 +00:00
• 42f1defd2a Split up some of Category (#72) Patrick Stevens 2019-11-13 20:14:52 +00:00
• d0f8d5ba39 Tidy up cyclic groups (#71) Patrick Stevens 2019-11-13 19:56:59 +00:00
• 8128733722 List uncompiled files (#70) Patrick Stevens 2019-11-13 19:01:33 +00:00
• 2ef7348d30 A bit of cleanup (#69) Patrick Stevens 2019-11-13 18:35:41 +00:00
• 4db82b1afc Tidy up groups more (#68) Patrick Stevens 2019-11-08 18:00:16 +00:00
• d30d14772e Fix up the structure of Actions and SymmetricGroups (#67) Patrick Stevens 2019-11-08 13:50:24 +00:00
• cac9d034c2 Move quotient group (#66) Patrick Stevens 2019-11-08 12:26:37 +00:00
• 82b81b4bab Elevate the real numbers to actually existing (#65) Patrick Stevens 2019-11-04 07:34:59 +00:00
• d95f510cdd Tidy up groups (#64) Patrick Stevens 2019-11-03 17:12:48 +00:00
• e4daab7153 Split out parts of Field of Fractions (#63) Patrick Stevens 2019-11-02 21:31:46 +00:00
• 1325236359 Rename order transitivity (#62) Patrick Stevens 2019-11-02 19:05:52 +00:00
• 763ddb8dbb Split partial and total order of rings (#61) Patrick Stevens 2019-11-02 18:42:37 +00:00
• 55995ea801 Minor perf improvements? (#60) Patrick Stevens 2019-11-02 08:57:15 +00:00
• a66080b8ae Reals form a ring (#59) Patrick Stevens 2019-11-02 08:34:09 +00:00
• df1ac6a303 Reals are a ring (#58) Patrick Stevens 2019-10-29 07:27:25 +00:00
• 92363f2be2 Real multiplication well-defined (#57) Patrick Stevens 2019-10-28 21:58:49 +00:00
• 553dd061d9 Approximate reals by rationals (#56) Patrick Stevens 2019-10-27 22:55:27 +00:00
• 0d68919127 Comparison on the reals (#55) Patrick Stevens 2019-10-26 10:36:24 +01:00
• 4e56b68024 Complete proof that sqrt 2 is irrational (#54) Patrick Stevens 2019-10-23 07:58:17 +01:00
• f5f4cf1376 Mostly show sqrt 2 is irrational (#53) Patrick Stevens 2019-10-22 20:56:58 +01:00
• 6eaa181104 Cauchy-completion, first parts (#52) Patrick Stevens 2019-10-22 07:51:09 +01:00
• 959071214e Rename some confusing fields (#51) Patrick Stevens 2019-10-13 09:31:54 +01:00
• 96d15c6017 Semiring solver (#50) Patrick Stevens 2019-10-12 11:14:27 +01:00
• 5af4030361 Rem extra args from identity (#49) Patrick Stevens 2019-10-03 07:21:30 +01:00
• 7ed41b0c09 Rearrange some of Naturals (#48) Patrick Stevens 2019-10-03 06:53:13 +01:00
• 21ee0f899d Primes and mod-n into the fold (#47) Patrick Stevens 2019-10-02 18:59:46 +01:00
• 00ce1dfdf8 Move equiv rels (#46) Patrick Stevens 2019-09-28 22:24:41 +01:00
• b92e6b2dd8 Implement subtraction on the binary naturals (#45) Patrick Stevens 2019-09-22 08:36:41 +01:00
• d4ebcc04ce Couple of useful Maybe functions (#44) Patrick Stevens 2019-09-15 15:08:51 +01:00
• 8c51b9b3d1 Finite product of countable sets is countable (#43) Patrick Stevens 2019-09-01 12:20:00 +01:00
• 9a24acbb0c Cantor pairing function is bijective (#42) Patrick Stevens 2019-09-01 10:23:25 +01:00
• 077ed6706a Rejig key-value (#41) Patrick Stevens 2019-08-24 08:40:27 +01:00
• 61f3dc7306 Move some more things over to Without K (#40) Patrick Stevens 2019-08-22 20:32:34 +01:00
• 9c14e7c439 Split out Integers and remove use of K (#39) Patrick Stevens 2019-08-22 08:37:41 +01:00