Ki Yung Ahn

> How to define mutually dependent classes with the IJava kernel? > ... > Any suggestions for a workaround? I find this annoying too, There is a workaround though. Define...

See https://github.com/SpencerPark/IJava/issues/101#issuecomment-666037959

This happens because the notebook metadata is not populated with enough information when it is created. ```json "language_info": { "name": "" } ``` When you change the above to below,...

Above is a very degenerate minimal example with the absurdity in the conclusion. The actual situation I came across was more close to like this. ``` Theorem lemmaGOOD : forall...

@chaudhuri Thanks for working on the fix and also for the tip to work around!

@chaudhuri Thanks to your tip on the workaround, I was able to prove the lemma I was working on. https://github.com/kyagrd/NonBisim2DF/tree/cbd059576a05e380bbd942b117487849051ba5ff/spi This is a real working example I came across this...

I actually came across the need for rewriting and had to resort to some hack, ignoring assumptions that may have capture problems and try to focus the "rewrite" on a...

Not a first order example but I've recently been working on formalizations of Intruder Deduction and Observer Theory and related proofs of some basic lemmas on consistency of the theories,...