OpenLogicProject / OpenLogic

An open-source, customizable intermediate logic textbook
http://openlogicproject.org/
Creative Commons Attribution 4.0 International
1.06k stars 240 forks source link

Redundant i in definition 14.10? #368

Closed marethyu closed 5 months ago

marethyu commented 6 months ago

I don't see where $i$ is used in $C=\blacktriangleright\smallfrown O\smallfrown \sqcup^j$. Perhaps, it is supposed to be written as $C=\blacktriangleright\smallfrown\sqcup^i \smallfrown O\smallfrown \sqcup^j$. Maybe add note that $\sqcup^n$ is a sequence of $n$ $\sqcup$s.

capture1