## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Aug 09 02:10

• Aug 07 14:26

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

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

comment tweaked (compare)

• Jul 27 10:14

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

corrected silly CI (compare)

• Jul 27 08:08

FreeModule sections (compare)

• Jul 27 05:29

• Jul 27 05:22

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

• Jul 27 00:47

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

• Jul 27 00:42

CI tweak (compare)

• Jul 27 00:36

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)

On the main branch is fine.
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.
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.
Once you do let me know the id or associated email
Anand
@0art0
I have created one with my IISER email ID
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.
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
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.
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.
I have pushed a sorry-free proof of the theorem about equality of folds of the two AddTrees.