Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Aug 09 02:10

    siddhartha-gadgil on v2.0-uc

    (compare)

  • Aug 07 14:26

    siddhartha-gadgil on unit-conjecture

    fun not lambdas Merge branch 'unit-conjecture' … (compare)

  • Aug 07 14:25

    0art0 on unit-conjecture

    Change from `\lambda` to `fun` … (compare)

  • Jul 29 15:11

    siddhartha-gadgil on unit-conjecture

    removing unused variables (compare)

  • Jul 27 13:08

    0art0 on unit-conjecture

    Change quotes to italics Indentation fix (compare)

  • Jul 27 11:20

    0art0 on unit-conjecture

    Push trivial proofs out of `Tor… Merge branch 'unit-conjecture' … (compare)

  • Jul 27 10:35

    siddhartha-gadgil on unit-conjecture

    comment tweaked (compare)

  • Jul 27 10:14

    siddhartha-gadgil on unit-conjecture

    tweak Merge branch 'unit-conjecture' … (compare)

  • Jul 27 09:30

    0art0 on unit-conjecture

    Change `apply Q.rec` -> `cases … (compare)

  • Jul 27 09:04

    0art0 on unit-conjecture

    Improved documentation for the … Merge documentation Add more documentation and 1 more (compare)

  • Jul 27 08:10

    siddhartha-gadgil on unit-conjecture

    corrected silly CI (compare)

  • Jul 27 08:08

    siddhartha-gadgil on unit-conjecture

    FreeModule sections (compare)

  • Jul 27 05:29

    siddhartha-gadgil on unit-conjecture

    headings in top docs (compare)

  • Jul 27 05:22

    siddhartha-gadgil on unit-conjecture

    top docs for all files, docs fo… (compare)

  • Jul 27 00:47

    siddhartha-gadgil on unit-conjecture

    Modify CI Modify CI further Make elan path explicit and 3 more (compare)

  • Jul 27 00:42

    siddhartha-gadgil on main

    CI tweak (compare)

  • Jul 27 00:36

    siddhartha-gadgil on unit-conjecture

    CI tweak Merge branch 'unit-conjecture' … (compare)

  • Jul 26 17:02

    0art0 on main

    Try building the mathlib folder… (compare)

  • Jul 26 16:51

    0art0 on main

    Make elan path explicit (compare)

  • Jul 26 16:49

    0art0 on main

    Modify CI further (compare)

Anand
@0art0
I have created a few files with descriptions, but I am having trouble pushing it to the repo since lake creates another .git within the subfolder.
For the time being, I will just put the descriptions up as GitHub issues.
Anand
@0art0
I have included a few potential topics for prompts. I can work on writing a few examples of each along with plaintext descriptions.
Siddhartha Gadgil
@siddhartha-gadgil
if that is an issue just move things to root.
The sub-folder was for neatness but not worth struggling over.
By the way, we are trying to add you to a "Team". Do you have a "Teams" account?
Anand
@0art0
I don't think I do, but I will create an account now.
Siddhartha Gadgil
@siddhartha-gadgil
Once you do let me know the id or associated email
Anand
@0art0
I have created one with my IISER email ID
Siddhartha Gadgil
@siddhartha-gadgil
I added you. Do you see the chat? Can you confirm there?
Anand
@0art0
I have added the folder with the Lean files. If it is too cluttered, I can try to revert the changes and do this on a separate branch.
Siddhartha Gadgil
@siddhartha-gadgil
It is fine.
Anand
@0art0
I think I finally managed to get the proof to work (in the case of lists). I will adapt it to the case of arrays and push the final code.
I used a helper lemma:
theorem List.get_index_eq : (l l' : List α) → (hl : l = l') → (i : ℕ) → (bnd : i < l.length) → l.get ⟨i, bnd⟩ = l'.get ⟨i, hl ▸ bnd⟩
  | _, _, rfl, _, _ => rfl
Siddhartha Gadgil
@siddhartha-gadgil
Excellent.
I have been focussing on the prompts for the AI stuff.
Anand
@0art0
I was planning to add some prompts related to function types and product types in the Foundations folder some time today. I will try to work on it after pushing the AddTree code.
Anand
@0art0
I was thinking of coming to IISc either tomorrow (before 10 AM, to attend the meeting from there) or on Friday.
Siddhartha Gadgil
@siddhartha-gadgil
I have autogenerated a lot of prompts, as you may have seen. You are welcome to add manual ones, but it is also fine to wait till we discuss so you can choose those with most bang for the buck.
Let me know when you come. We can meet on Friday if you come then, to discuss the simplification tactics and a few other things. Tomorrow I will join the meeting from home, but if you are around post lunch (say 1:30 or later) we can meet then.
Anand
@0art0
I think I will come on Friday since there is a good chance of finishing a large portion of the AddTreecode by then. I will come in the morning at around 10:30 AM and stay for a while.
Siddhartha Gadgil
@siddhartha-gadgil
That sounds good.
I will meet you then.
Anand
@0art0
I have pushed a sorry-free proof of the theorem about equality of folds of the two AddTrees.
Siddhartha Gadgil
@siddhartha-gadgil
Excellent. Will look at it.