Marcus Rossel
Marcus Rossel
This PR implements a TODO for throwing an error on `dsimp` arguments which aren't proofs by reflexivity. I don't know exactly what `resolveSimpIdTheorem?` does, so there might be some cases...
https://github.com/mkroetzsch/TheoLog/blob/420dd69fa4f033aa292fc9738f95800151fe6801/Vorlesungen/lecture-06.tex#L285 Ich bin mir nicht ganz sicher ob dies stimmt, aber ist das Schnittproblem für Typ-{0, 1, 2}-Grammatiken wirklich semi-entscheidbar, wenn _Schnitt_ durch "L(G1) ∩ L(G2) = ∅" definiert ist?...
This PR adds documentation comments for a few functions in `lean.h`. This was previously discussed at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structure.20in.20FFI/near/431985775 I think it would be good if someone knowledgable (@digama0?) could check that...