## Project Report for Logic, Types, Spaces 2019

### Outline of the work done

Please fill in this with references to code.

# Project report LTS2019

## Algebra

### Fields.idr

1. made a modified definition InvExistsNonZero, the type of proofs that non zero elements of a field have multiplicative inverses.
2. Using this definition for a modified multiplicative inverse, IsModGrp is the type of proofs that non zero elements of a field form a group over multiplication.
3. Using this, IsField is the type of proofs that a given type with “additions” and “multiplication” appropriately defined on them form a field.

### Finitely Generated Groups Group.FiniteGenerate.idr

1. Created the file on finitely generated groups, with HasFiniteOrder proving that an element is finitely generated. Have to further work on it once primes have been defined with the appropriate properties.

## Number Theory

### Primes.idr

1. IsPrime and IsComposite types are the types of proofs that a number is prime or composite respectively.
2. twoPr shows that two is a prime to verify the functioning of the IsPrime type.
3. Proved that a number cannot be both prime and composite using notBothPrimeandComp, which utilises a helper function aNotEqToMultA (a not equal to na, where n is greater than 1).
4. genFact generates a list of factors of a number along with the proof that they are factors.
5. isPrimeCalc and isCompositeCalc check for primality of a number computationally.

## Utility files (Lists.idr)

1. Created a file on lists to extract useful results from the genFact function mentioned earlier.

### Pending (for now)

1. To show that any number greater than 2 is either prime or Composite. (Partially done, proof that number is composite based on genFact size has been included)
2. To show that every divisor of a number is contained within the genFact list.

### Log of git commits by author


commit 9c0a5615d9bf4a0853013c4208d79dbe3619e5a8
Author:     Sidharth Soundararajan
AuthorDate: Mon Apr 22 12:49:29 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Mon Apr 22 12:49:29 2019 +0530

update

.DS_Store                                          |   Bin 8196 -> 8196 bytes
.../0/B5465627D307BC93E8CC09C2977823BA25484925.gpg |   Bin
.../0/FEA1BE7D65D124C05693213EF0C5A0DF8B5FC01E.gpg |   Bin
Assignments/Basen.idr                              |   Bin 0 -> 1906 bytes
Assignments/Bezout.idr                             |   Bin 0 -> 1653 bytes
Assignments/ChinmayaOdds.idr                       |   Bin 0 -> 1814 bytes
Assignments/Evens.idr                              |   Bin 0 -> 2082 bytes
Assignments/InsertionSort.idr                      |   Bin 0 -> 674 bytes
Assignments/Intro.idr                              |   Bin 0 -> 966 bytes
Assignments/MyAss1.idr                             |   Bin 0 -> 495 bytes
Assignments/NatTree.idr                            |   Bin
Assignments/RecRule.idr                            |   Bin 0 -> 998 bytes
Assignments/Tuple.idr                              |   Bin 0 -> 212 bytes
Assignments/arkasparko/Evens.idr                   |    74 +
Assignments/arkasparko/Intro.idr                   |    48 +
Assignments/arkasparko/Odd.idr                     |    99 +
Assignments/biswajitnag/Assignement1/Evens.idr     |    74 +
Assignments/biswajitnag/Assignement1/Intro.idr     |    48 +
Assignments/biswajitnag/Assignement1/desktop.ini   |     5 +
Assignments/biswajitnag/Assignement1/first.idr     |    65 +
Assignments/merge.idr                              |   Bin 0 -> 1308 bytes
Assignments/nabarundeka/Assignment1/Evens.idr      |    74 +
Assignments/nabarundeka/Assignment1/Intro.idr      |    48 +
.../nabarundeka/Assignment1/nabarundeka.idr        |    53 +
Assignments/piyushsati/Assignment1/Evens.idr       |    75 +
Assignments/piyushsati/Assignment1/Intro.idr       |    49 +
.../piyushsati/Assignment1/OddsAndEvens.idr        |    72 +
Assignments/rohitkumar-odds.idr                    |   Bin 0 -> 1884 bytes
Assignments/shafiln/Evens.idr                      |    74 +
Assignments/shafiln/Intro.idr                      |    48 +
Assignments/shafiln/assignment.idr                 |    59 +
Assignments/sidharths/lts/Assignment1.idr          |    43 +
Assignments/sidharths/lts/Evens.idr                |    74 +
Assignments/sidharths/lts/Intro.idr                |    48 +
Assignments/sorting_with_proof.idr                 |   Bin 0 -> 2260 bytes
Assignments/srirams/Odds and Evens/Evens.idr       |    74 +
Assignments/srirams/Odds and Evens/Intro.idr       |    48 +
.../srirams/Odds and Evens/Srirams.Odds.idr        |    60 +
Assignments/sum.sc                                 |   Bin 0 -> 721 bytes
Assignments/test.txt                               |   Bin 0 -> 28 bytes
Assignments/vrundarathi/Evens.idr                  |    74 +
Assignments/vrundarathi/Intro.idr                  |     1 +
Assignments/vrundarathi/VrundaOdd.idr              |    62 +
Code/AbishekRajanAssRecRule.idr                    |     0
Code/All_is_Refl.idr                               |     0
Code/ArkaAssRecRule.idr                            |     0
Code/AssRecRule.idr                                |     0
Code/Bezout.idr                                    |   155 +
Code/BoundedGCD.idr                                |     0
Code/ChinmayaKausikAssRecRule.idr                  |     0
Code/Choice.idr                                    |     3 +
Code/DecOrderNat.idr                               |     0
Code/ExpressionParser.idr                          |     0
Code/Field.idr                                     |    30 +
Code/FieldAxioms.idr                               |     0
Code/FinUtils.idr                                  |     0
Code/Finite.idr                                    |    36 +
Code/FreeGroup.idr                                 |     0
Code/Graph.idr                                     |   142 +
Code/Graph_alt.idr                                 |     0
Code/Graphexamples.idr                             |     0
Code/Group.FiniteGenerate.idr                      |    26 +
Code/Group.idr                                     |    73 +
Code/Group_property.idr                            |   129 +
Code/Group_property2.idr                           |    81 +
Code/Group_property3.idr                           |    47 +
Code/HackyLang.idr                                 |     0
Code/InsertionHelpers.idr                          |     0
Code/InsertionProof.idr                            |     0
Code/InsertionSort.idr                             |     0
Code/LTE_Properties.idr                            |     0
Code/Lecture.GCD.idr                               |    20 +
Code/Lecture.Intro.idr                             |    58 +
Code/Lecture.NatTree.idr                           |    53 +
Code/Lecture.RecRule.idr                           |    46 +
Code/Lecture.Tuple.idr                             |    12 +
Code/LectureEvens.idr                              |    88 +
Code/Linear.idr                                    |     0
Code/LinearAlgebra.idr                             |     0
Code/LittleInterpreter.idr                         |     0
Code/LittleLang.idr                                |     0
Code/Matrix.idr                                    |    56 +
Code/Merge.idr                                     |   179 +
Code/Monoid.idr                                    |    36 +
Code/MultiSolver.idr                               |   184 +
Code/Order.idr                                     |     0
Code/Parsers.idr                                   |     0
Code/PermCons.idr                                  |     0
Code/PermConsProperties.idr                        |     0
Code/Permutation.idr                               |    59 +
Code/Primes.idr                                    |     0
Code/Product_Type_Eq.idr                           |     0
Code/Q.idr                                         |     0
Code/Quotient_Group.idr                            |    65 +
Code/Quotient_Type.idr                             |     0
Code/Rationals.idr                                 |     0
Code/Rats.idr                                      |     0
Code/Relations.idr                                 |     0
Code/Ring.idr                                      |   153 +
Code/RingExamples.idr                              |     0
Code/RohitKumarAssRecRule2.idr                     |     0
Code/Scheme_Expressions.idr                        |     0
Code/Scheme_Parsers.idr                            |     0
Code/ShafilMaheenNAssRecRule.idr                   |     0
Code/SidharthAssRecRule.idr                        |     0
Code/Sign.idr                                      |    39 +
Code/SortingWithProof.idr                          |     0
Code/SriramAssRecRule.idr                          |     0
Code/TwoVarDiophEq.idr                             |     0
Code/VrundaAssRecRule.idr                          |     0
Code/ZZUtils.idr                                   |     0
Code/ZZ_alt.idr                                    |     0
Code/ZZmult.idr                                    |     0
Code/ZZsubs.idr                                    |     0
Code/check-all.sh                                  |     5 +
Code/congruence.idr                                |     0
Code/decDivZ.idr                                   |     0
Code/fn_to_vect.idr                                |    74 +
Code/midterm-check.txt                             |    85 +
Code/nabarunAssRecRule.idr                         |     0
Code/pigeonhole.idr                                |     0
Code/rationals/Rationals.idr                       |    29 +
Code/sum.sc                                        |    40 +
Code/total-check-all.sh                            |     5 +
Dockerfile                                         |     4 +
Gemfile                                            |    25 +
Gemfile.lock                                       |    77 +
GitHub-Mark-Light-32px.png                         |   Bin 0 -> 1571 bytes
IIScLogo.jpg                                       |   Bin 0 -> 51171 bytes
Rakefile                                           |    23 +
Voevodsky.WhyHoTT.pdf                              |   Bin 0 -> 1514461 bytes
_announcements/project.md                          |     0
_assignments/odds.md                               |    25 +
_assignments/rec.md                                |     0
_config-local.yml                                  |     1 +
_config-production.yml                             |    14 +
_config.yml                                        |     0
_draft-assignments/am-gm.md                        |     0
_draft-assignments/conics.md                       |    23 +
_draft-assignments/gram-schmidt.md                 |     0
_draft-assignments/laplacian.md                    |    15 +
_draft-assignments/liouville.md                    |     0
_draft-assignments/partial-total.md                |     0
_draft-assignments/van-der-monde.md                |     0
_includes/footer.html                              |    21 +
_layouts/assignment.html                           |    18 +
_layouts/default.html                              |     5 +
_layouts/draft-assignment.html                     |    11 +
_layouts/notes.html                                |    14 +
_layouts/report.html                               |    17 +
_local-site/Assignments/Basen.idr                  |    55 +
_local-site/Assignments/Bezout.idr                 |    36 +
_local-site/Assignments/ChinmayaOdds.idr           |    60 +
_local-site/Assignments/Evens.idr                  |    75 +
_local-site/Assignments/InsertionSort.idr          |    24 +
_local-site/Assignments/Intro.idr                  |    53 +
_local-site/Assignments/MyAss1.idr                 |    21 +
_local-site/Assignments/NatTree.idr                |    53 +
_local-site/Assignments/RecRule.idr                |    37 +
_local-site/Assignments/Tuple.idr                  |    12 +
_local-site/Assignments/arkasparko/Evens.idr       |    74 +
_local-site/Assignments/arkasparko/Intro.idr       |    48 +
_local-site/Assignments/arkasparko/Odd.idr         |    99 +
.../Assignments/biswajitnag/Assignement1/Evens.idr |    74 +
.../Assignments/biswajitnag/Assignement1/Intro.idr |    48 +
.../biswajitnag/Assignement1/desktop.ini           |     5 +
.../Assignments/biswajitnag/Assignement1/first.idr |    65 +
_local-site/Assignments/merge.idr                  |    39 +
.../Assignments/nabarundeka/Assignment1/Evens.idr  |    74 +
.../Assignments/nabarundeka/Assignment1/Intro.idr  |    48 +
.../nabarundeka/Assignment1/nabarundeka.idr        |    53 +
_local-site/Assignments/odds.html                  |   255 +
.../Assignments/piyushsati/Assignment1/Evens.idr   |    75 +
.../Assignments/piyushsati/Assignment1/Intro.idr   |    49 +
.../piyushsati/Assignment1/OddsAndEvens.idr        |    72 +
_local-site/Assignments/rohitkumar-odds.idr        |    50 +
_local-site/Assignments/shafiln/Evens.idr          |    74 +
_local-site/Assignments/shafiln/Intro.idr          |    48 +
_local-site/Assignments/shafiln/assignment.idr     |    59 +
.../Assignments/sidharths/lts/Assignment1.idr      |    43 +
_local-site/Assignments/sidharths/lts/Evens.idr    |    74 +
_local-site/Assignments/sidharths/lts/Intro.idr    |    48 +
_local-site/Assignments/sorting_with_proof.idr     |    80 +
.../Assignments/srirams/Odds and Evens/Evens.idr   |    74 +
.../Assignments/srirams/Odds and Evens/Intro.idr   |    48 +
.../srirams/Odds and Evens/Srirams.Odds.idr        |    60 +
_local-site/Assignments/sum.sc                     |    40 +
_local-site/Assignments/test.txt                   |     1 +
_local-site/Assignments/vrundarathi/Evens.idr      |    74 +
_local-site/Assignments/vrundarathi/Intro.idr      |     1 +
_local-site/Assignments/vrundarathi/VrundaOdd.idr  |    62 +
_local-site/Code/BaseN.idr                         |   151 +
_local-site/Code/Bezout.idr                        |   155 +
_local-site/Code/Choice.idr                        |     3 +
_local-site/Code/Divisors.idr                      |   193 +
_local-site/Code/Field.idr                         |    30 +
_local-site/Code/FinUtils.idr                      |    39 +
_local-site/Code/Finite.idr                        |    36 +
_local-site/Code/GCDZZ.idr                         |    52 +
_local-site/Code/Graph.idr                         |   142 +
_local-site/Code/Graph_alt.idr.fixme               |    45 +
_local-site/Code/Graphexamples.idr                 |    33 +
_local-site/Code/Group.FiniteGenerate.idr          |    26 +
_local-site/Code/Group.idr                         |    73 +
_local-site/Code/GroupCosetRep.idr                 |    29 +
_local-site/Code/GroupCosets.idr                   |    45 +
_local-site/Code/Group_property.idr                |   129 +
_local-site/Code/Group_property2.idr               |    86 +
_local-site/Code/InsertionSort.idr                 |    39 +
_local-site/Code/Lecture.GCD.idr                   |    20 +
_local-site/Code/Lecture.Intro.idr                 |    58 +
_local-site/Code/Lecture.NatTree.idr               |    53 +
_local-site/Code/Lecture.RecRule.idr               |    46 +
_local-site/Code/Lecture.Tuple.idr                 |    12 +
_local-site/Code/LectureEvens.idr                  |    88 +
_local-site/Code/Linear.idr                        |   129 +
_local-site/Code/LinearAlgebra.idr                 |   210 +
_local-site/Code/Lists.idr                         |    30 +
_local-site/Code/Merge.idr                         |   179 +
_local-site/Code/Monoid.idr                        |    36 +
_local-site/Code/MultiSolver.idr                   |   184 +
_local-site/Code/NatOrder.idr                      |   229 +
_local-site/Code/NatUtils.idr                      |   233 +
_local-site/Code/Order.idr                         |   120 +
_local-site/Code/PermCons.idr                      |    22 +
_local-site/Code/Permutation.idr                   |    59 +
_local-site/Code/Primes.idr                        |   361 +
_local-site/Code/Quicksort.idr                     |    13 +
_local-site/Code/Quotient_Group.idr                |    65 +
_local-site/Code/Rationals.idr                     |   119 +
_local-site/Code/Ring.Properties.idr               |    40 +
_local-site/Code/Ring.idr                          |   153 +
_local-site/Code/Sign.idr                          |    39 +
_local-site/Code/SortingWithProof.idr              |    36 +
_local-site/Code/ZZ.idr                            |   515 +
_local-site/Code/ZZUtils.idr                       |    61 +
_local-site/Code/check-all.sh                      |     5 +
_local-site/Code/congruence.idr                    |     6 +
_local-site/Code/fn_to_vect.idr                    |    74 +
_local-site/Code/gcd.idr                           |    92 +
_local-site/Code/midterm-check.txt                 |    85 +
_local-site/Code/pigeonhole.idr                    |    80 +
_local-site/Code/rationals/Rationals.idr           |    29 +
_local-site/Code/sum.sc                            |    40 +
_local-site/Dockerfile                             |     4 +
_local-site/Gemfile                                |    25 +
_local-site/Gemfile.lock                           |    77 +
_local-site/GitHub-Mark-Light-32px.png             |   Bin 0 -> 1571 bytes
_local-site/IIScLogo.jpg                           |   Bin 0 -> 51171 bytes
_local-site/Rakefile                               |    23 +
_local-site/Voevodsky.WhyHoTT.pdf                  |   Bin 0 -> 1514461 bytes
_local-site/am-gm.md                               |     0
_local-site/announce-all.html                      |   226 +
_local-site/assets/main.css                        |   501 +
_local-site/assets/minima-social-icons.svg         |    33 +
_local-site/assign-all.html                        |   256 +
_local-site/bezout.idr                             |   204 +
_local-site/css/bootstrap-grid.css                 |  1912 +++
_local-site/css/bootstrap-grid.css.map             |     1 +
_local-site/css/bootstrap-grid.min.css             |     7 +
_local-site/css/bootstrap-grid.min.css.map         |     1 +
_local-site/css/bootstrap-reboot.css               |   331 +
_local-site/css/bootstrap-reboot.css.map           |     1 +
_local-site/css/bootstrap-reboot.min.css           |     8 +
_local-site/css/bootstrap-reboot.min.css.map       |     1 +
_local-site/css/bootstrap-theme.css                |   587 +
_local-site/css/bootstrap-theme.css.map            |     1 +
_local-site/css/bootstrap-theme.min.css            |     6 +
_local-site/css/bootstrap-theme.min.css.map        |     1 +
_local-site/css/bootstrap.bundle.js.map            |     1 +
_local-site/css/bootstrap.bundle.min.js.map        |     1 +
_local-site/css/bootstrap.css                      |  6757 ++++++++++
_local-site/css/bootstrap.css.map                  |     1 +
_local-site/css/bootstrap.js.map                   |     1 +
_local-site/css/bootstrap.min.css                  |    11 +
_local-site/css/bootstrap.min.css.map              |     1 +
_local-site/css/bootstrap.min.js.map               |     1 +
_local-site/css/default.css                        |   155 +
_local-site/css/extras.css                         |     7 +
_local-site/css/main.css                           |   501 +
_local-site/css/materialize.css                    |  9067 ++++++++++++++
_local-site/css/materialize.min.css                |    13 +
_local-site/css/zenburn.css                        |   118 +
_local-site/deploy                                 |     2 +
_local-site/draft-assignments/conics.html          |   254 +
_local-site/draft-assignments/laplacian.html       |   243 +
_local-site/feed.xml                               |    42 +
_local-site/gitlog                                 |   276 +
_local-site/gram-schmidt.md                        |     0
_local-site/index.html                             |   328 +
.../update/2017/02/03/welcome-to-jekyll.html       |   248 +
_local-site/js/bootstrap.bundle.js                 |  6461 ++++++++++
_local-site/js/bootstrap.bundle.js.map             |     1 +
_local-site/js/bootstrap.bundle.min.js             |     7 +
_local-site/js/bootstrap.bundle.min.js.map         |     1 +
_local-site/js/bootstrap.js                        |  2377 ++++
_local-site/js/bootstrap.js.map                    |     1 +
_local-site/js/bootstrap.min.js                    |     7 +
_local-site/js/bootstrap.min.js.map                |     1 +
_local-site/js/highlight.js                        |    30 +
_local-site/js/materialize.js                      | 12374 +++++++++++++++++++
_local-site/js/materialize.min.js                  |     6 +
_local-site/js/npm.js                              |    13 +
_local-site/liouville.md                           |     0
_local-site/local.sh                               |     1 +
_local-site/midterm-check.txt                      |     0
_local-site/notes-all.html                         |   246 +
_local-site/notes/foundations.html                 |   289 +
_local-site/notes/meta.html                        |   231 +
_local-site/notes/types-topics.html                |   277 +
_local-site/partial-total.md                       |     0
_local-site/reports/ar.html                        |   772 ++
_local-site/reports/arka.html                      |   697 ++
_local-site/reports/chinmaya.html                  |   855 ++
_local-site/reports/nabarun.html                   |   330 +
_local-site/reports/rathivrunda.html               |   320 +
_local-site/reports/rohit.html                     |   322 +
_local-site/reports/shafil.html                    |   976 ++
_local-site/reports/sideart.html                   |   426 +
_local-site/reports/ss.html                        |   560 +
_local-site/test.sh                                |     9 +
_local-site/update-git                             |    11 +
_local-site/van-der-monde.md                       |     0
_notes/foundations.md                              |    57 +
_notes/languages-and-limits.md                     |     0
_notes/meta.md                                     |     6 +
_notes/types-topics.md                             |    32 +
_posts/2017-02-03-welcome-to-jekyll.markdown       |    25 +
_reports/nabarun/nabarun.md                        |    23 +
_reports/shafil/gitlog                             |     0
_reports/shafil/shafil.md                          |     0
_reports/sideart/gitlog                            |   150 +
_reports/sideart/sideart.md                        |    38 +
announce-all.html                                  |    16 +
assign-all.html                                    |    18 +
css/bootstrap-grid.css                             |  1912 +++
css/bootstrap-grid.css.map                         |     1 +
css/bootstrap-grid.min.css                         |     7 +
css/bootstrap-grid.min.css.map                     |     1 +
css/bootstrap-reboot.css                           |   331 +
css/bootstrap-reboot.css.map                       |     1 +
css/bootstrap-reboot.min.css                       |     8 +
css/bootstrap-reboot.min.css.map                   |     1 +
css/bootstrap-theme.css                            |   587 +
css/bootstrap-theme.css.map                        |     1 +
css/bootstrap-theme.min.css                        |     6 +
css/bootstrap-theme.min.css.map                    |     1 +
css/bootstrap.bundle.js.map                        |     1 +
css/bootstrap.bundle.min.js.map                    |     1 +
css/bootstrap.css                                  |  6757 ++++++++++
css/bootstrap.css.map                              |     1 +
css/bootstrap.js.map                               |     1 +
css/bootstrap.min.css                              |    11 +
css/bootstrap.min.css.map                          |     1 +
css/bootstrap.min.js.map                           |     1 +
css/default.css                                    |   155 +
css/extras.css                                     |     0
css/main.scss                                      |    39 +
css/materialize.css                                |  9067 ++++++++++++++
css/materialize.min.css                            |    13 +
css/zenburn.css                                    |   118 +
deploy                                             |     2 +
feed.xml                                           |    30 +
index.html                                         |   115 +
js/bootstrap.bundle.js                             |  6461 ++++++++++
js/bootstrap.bundle.js.map                         |     1 +
js/bootstrap.bundle.min.js                         |     7 +
js/bootstrap.bundle.min.js.map                     |     1 +
js/bootstrap.js                                    |  2377 ++++
js/bootstrap.js.map                                |     1 +
js/bootstrap.min.js                                |     7 +
js/bootstrap.min.js.map                            |     1 +
js/highlight.js                                    |    30 +
js/materialize.js                                  | 12374 +++++++++++++++++++
js/materialize.min.js                              |     6 +
js/npm.js                                          |    13 +
local.sh                                           |     1 +
notes-all.html                                     |    14 +
update-git                                         |    11 +
400 files changed, 103334 insertions(+)

Author:     Sidharth Soundararajan
AuthorDate: Mon Apr 22 12:36:50 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Mon Apr 22 12:36:50 2019 +0530

eitherPrimeOrComp partially done

.DS_Store           | Bin 6148 -> 6148 bytes
Code/Order.idr      | 120 ++++++++++++++++++++++++++++++++++++++++++++++++++++
Code/PrimeApple.idr |  31 ++++++++++----
3 files changed, 143 insertions(+), 8 deletions(-)

commit f350d5605e42e3fac009c8296648500bc4c36fdb
Author:     Sidharth Soundararajan
AuthorDate: Thu Apr 11 10:37:14 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Thu Apr 11 10:37:14 2019 +0530

update

Code/Lists.idr  |   1 -
Code/Primes.idr | 753 ++++++++++++++++++++++++++++----------------------------
2 files changed, 382 insertions(+), 372 deletions(-)

commit 92d14bc5d84aa79bb295a38720018890365002a6
Author:     Sidharth Soundararajan
AuthorDate: Sat Mar 2 18:39:46 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Sat Mar 2 18:39:46 2019 +0530

Update

Code/Group.FiniteGenerate.idr |  4 ++--
Code/Lists.idr                |  1 +
Code/Primes.idr               | 16 +++++++++++-----
3 files changed, 14 insertions(+), 7 deletions(-)

commit 2846bef2c91decaeea6e1a101a384495ab04675e
Author:     Sidharth Soundararajan
AuthorDate: Mon Feb 25 18:32:10 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Mon Feb 25 18:32:10 2019 +0530

Update sideart.md

_reports/sideart/sideart.md | 28 +++++++++++++++-------------
1 file changed, 15 insertions(+), 13 deletions(-)

commit dbd83a440bcfce34a3ab346802aef2ffc65e4572
Author:     Sidharth Soundararajan
AuthorDate: Sun Feb 24 20:54:48 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Sun Feb 24 20:54:48 2019 +0530

added more functions to primes, created lists file

Code/Lists.idr              |  9 +++++++++
Code/Primes.idr             | 24 +++++++++++++++++++++---
_reports/sideart/sideart.md | 30 ++++++++++++++++++++++++++++++
3 files changed, 60 insertions(+), 3 deletions(-)

commit 29b47f98a3703fe20f078ee1361e69403d36a4de
Author:     Sidharth Soundararajan
AuthorDate: Sun Feb 24 15:31:26 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Sun Feb 24 15:31:26 2019 +0530

Update NatUtils.idr

Code/NatUtils.idr | 2 ++
1 file changed, 2 insertions(+)

commit 9c94ff6b87b827f723788dce5df6a88291564ec2
Author:     Sidharth Soundararajan
AuthorDate: Sun Feb 24 03:20:38 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Sun Feb 24 03:20:38 2019 +0530

redefined primes

redefined primes (removed them as data type), and created functions to show that a number cannot be both prime and composite

Code/Primes.idr | 20 ++++++++++++++++----
1 file changed, 16 insertions(+), 4 deletions(-)

commit 60967574f5ae4141f78ea4ee5ffa7edda3129583
Author:     Sidharth Soundararajan
AuthorDate: Sun Feb 24 01:08:15 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Sun Feb 24 01:08:15 2019 +0530

corrected primes

Code/Group.idr    |  1 -
Code/NatUtils.idr |  9 +++++++
Code/Primes.idr   | 71 ++++++++++++++++++++++++++++++++++++++++++++++---------
3 files changed, 69 insertions(+), 12 deletions(-)

commit cd372cc4b8af243ff69a02816aaabcb527410623
Author:     Sidharth Soundararajan
AuthorDate: Sat Feb 23 14:17:55 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Sat Feb 23 14:17:55 2019 +0530

Code/Graph_alt.idr                            |  45 +++++++++
Group.CosetRep.idr => Code/Group.CosetRep.idr |  13 ++-
Code/Group.FiniteGenerate.idr                 |   4 +-
Code/NatOrder.idr                             | 139 ++++++++++++++++++++++++++
Code/NatUtils.idr                             |  15 ++-
Code/Primes.idr                               |  72 ++++---------
Code/fn_to_vect.idr                           |  74 ++++++++++++++
_reports/arka/gitlog                          |  44 ++++++++
_reports/chinmaya/gitlog                      |  79 +++++++++++++++
_reports/nabarun/gitlog                       |  33 ++++++
_reports/ss/gitlog                            |  47 +++++++++
12 files changed, 607 insertions(+), 67 deletions(-)

commit 56ffb1128840ea38549d4e6791bda9befcc78e43
Author:     Sidharth Soundararajan
AuthorDate: Fri Feb 22 15:07:14 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Fri Feb 22 15:07:14 2019 +0530

have to clean the code

Code/Primes.idr | 42 +++++++++++++++++++++++++-----------------
1 file changed, 25 insertions(+), 17 deletions(-)

commit 677a7bddcc9cc810ea419fcae5b794cb39f14483
Author:     Sidharth Soundararajan
AuthorDate: Wed Feb 20 20:45:10 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Wed Feb 20 20:45:10 2019 +0530

Update Primes.idr

Code/Primes.idr | 21 ++++++++++++++++++---
1 file changed, 18 insertions(+), 3 deletions(-)

commit 804e287d355333a5dcf32c942cefa3c16f7ac50d
Author:     Sidharth Soundararajan
AuthorDate: Wed Feb 20 16:19:38 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Wed Feb 20 16:19:38 2019 +0530

create list with factors of numbers and check if number is prime

Code/Primes.idr | 50 ++++++++++++++++++++++++--------------------------
1 file changed, 24 insertions(+), 26 deletions(-)

commit 044be5279e8bd8dfb4325f4e13d4d2e66136c7a2
Author:     Sidharth Soundararajan
AuthorDate: Thu Feb 14 16:55:52 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Thu Feb 14 16:55:52 2019 +0530

Created file for finitely generated abelian groups project

.DS_Store                     | Bin 0 -> 8196 bytes
Code/Group.FiniteGenerate.idr |  26 ++++++++++++++++++++++++++
2 files changed, 26 insertions(+)

commit b9c13142932c1fbfb04b1e9e9e9e1173f5cd818f
Author:     Sidharth Soundararajan
AuthorDate: Sun Feb 10 22:05:12 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Sun Feb 10 22:05:12 2019 +0530

Corrected error in definition of Field (multiplicatiove inverse requires non zero elements)

Code/Field.idr | 24 +++++++++++++++++++++---
Code/Group.idr | 28 ++++++++++++++--------------
2 files changed, 35 insertions(+), 17 deletions(-)

commit e95b0ba8fec866be5370bd3fd843894b607ffd7a
Author:     Sidharth Soundararajan
AuthorDate: Sat Feb 9 19:50:36 2019 +0530
Commit:     Sidharth Soundararajan
CommitDate: Sat Feb 9 19:50:36 2019 +0530

Create Field.idr

Code/Field.idr | 12 ++++++++++++
1 file changed, 12 insertions(+)