Syntax errors in Lean4 using Markus Himmel's paper

Stream: lean4

[Daniel Donnelly]

image.png

Using the document here:
https://pp.ipd.kit.edu/uploads/publikationen/himmel20bachelorarbeit.pdf

How can I begin to create categories / diagram chase proofs in Lean4? Thanks. This document seems outdated

[Eric Wieser]

The code in that document is Lean3

[Eric Wieser]

The error you're getting is because Type* syntax is provided by some part of Mathlib, for which you need an import (import Mathlib.Tactic will do)

[Daniel Donnelly]

@Eric Wieser How can I learn diagram chasing in Lean4 if there is no corresponding document?

[Daniel Donnelly]

Eric Wieser said:

The error you're getting is because Type* syntax is provided by some part of Mathlib, for which you need an import (import Mathlib.Tactic will do)

image.png

[Daniel Donnelly]

@Eric Wieser NVM, found this: https://leanprover-community.github.io/install/project.html

[Eric Wieser]

Perhaps import should give a special error message with that link if the path starts with Mathlib

[Eric Wieser]

(and maybe Std too for good measure)