Using lean as a logical framework

Stream: Is there code for X?

[Poscat]

Are there any attempts at using lean as a logical framework similar to Isabelle?

[Luigi Massacci]

Not that I have ever seen, and I would be surprised if there have been any.

[Shreyas Srinivas]

Arguably iris-lean is doing that by embedding the logic of iris into lean

[Shreyas Srinivas]

Also I know of at least one other somewhat serious attempt at embedding another proof assistant inside lean

[Shreyas Srinivas]

So I wouldn’t be surprised to learn of other such attempts

[Poscat]

Shreyas Srinivas said:

Arguably iris-lean is doing that by embedding the logic of iris into lean

Is it ergonomic :monocle:

[Poscat]

Seems pretty alright https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/Examples/Proofs.lean