greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Ignore backup files

Browse Source 
Files ending with a tilde suffix are backups.
This commit is contained in:
Bulhwi Cha
2024-10-18 16:09:28 +09:00
parent 66b27f382a
commit f9f1597a06
2 changed files with 1 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@@ -3,3 +3,4 @@ lake-packages/
.lake/ .lake/
**/.DS_Store **/.DS_Store
.i18n/**/*.mo .i18n/**/*.mo
*~

15
vid_script.txt~
View File

@@ -1,15 +0,0 @@
How I made the natural number game.
Peter Johnstone taught me that 0 was {}, 1 was {{}}, 2 was {{},{{}}} and so on. But what about all the people who didn't go to that class?
Set theory is *one way of doing mathematics*.
Type theory is *another way of doing mathematics*
In mathematics, when you say "let G be a group" what you mean is that G is a set, and G has elements, and the elements are all individual "atoms", and that it is impossible to split the atom.
A theorem
Load of old nonsense.
IDeas: geometry game,