Stream: Beginner Questions

Topic: Stating a theorem like the "simps"

Yiming Xu (Nov 01 2024 at 09:25):

After defining a recursive function, I can type, say, csatis.simps in my case to get this fun

image.png

If I would like to prove an alternative definition, and I would like the same format, in the sense of if I type thm csatis_alt, it still gives me this five dots. What should I type when stating the theorem to be proved?

It seems not the &&&. For instance, I tried

lemma csatis_simps1:"
A &&& B
" sorry

and I typed thm csatis_simps1. It just says A &&& B, instead of giving me two "dots".

Mathias Fleury (Nov 01 2024 at 10:27):

lemma cstatis_simps:
   "A"
   "B"
   "C"

Yiming Xu (Nov 01 2024 at 10:47):

That works, thanks!!!

Last updated: Nov 07 2025 at 12:43 UTC