Repository navigation

Add pt-BR translation - #1

Closed

felipponn wants to merge 16 commits into

TentativeConvert:mainfrom

Commits on Dec 27, 2025

chore: Update link to lean 3 version of the natural number game to point to the frozen game repo (#126)
Osalotioman
authored
90902a7
2 typos (#123)
TentativeConvert
authored
1853318
"Leave World" button is now called "Home" (#120)
TentativeConvert
authored
7dc9e92
stray quotation mark at the end of definition of Add (#121)
TentativeConvert
authored
7af99fd
Fix minor spelling error in L3 of Implication World (#124)
vatrat
authored
d593c1e

Commits on Mar 1, 2026

chore: update button text from 'Leave World' to 'Home' (#127)
he7d3r
authored
6367e71

Commits on Mar 16, 2026

Commits on May 23, 2026

Minor documentation improvements (#136)
marlycormar
authored
dfa53e9
Leave World -> Home (#150)
comods
authored
fdef6fe

Commits on Jul 3, 2026

Fix few typos (#156)
jhrcek
authored
727e4d2

Commits on Aug 30, 2026

Fix typos in L06intro.lean (#168)
armgabrielyan
authored
360d797

Commits on Sep 8, 2026

Start translation to pt-BR
felipponn
committed
b0d93b1
Finish pt-BR translation
felipponn
committed
f998483