Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
$ linja
[2/6] "/usr/local/Cellar/lean/" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/TypeEqu.ilean"
FAILED: "/usr/local/Cellar/lean/" /Users/5HT/depot/groupoid/exe/prelude/lean/TypeEqu.lean -o "/Users/5HT/depot/groupoid/exe/prelude/lean/TypeEqu.olean" -c "/Users/5HT/depot/groupoid/exe/prelude/lean/TypeEqu.clean" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/TypeEqu.ilean"
/Users/5HT/depot/groupoid/exe/prelude/lean/TypeEqu.lean:8:7: error: type mismatch at definition 'TypeEqu', has type
Type.{u+1} → Type.{u+1} → Type.{imax (u+2) (imax (u+2) u) (imax (u+2) (u+2) (u+2) u) (imax (u+2) (u+2) u) u}
but is expected to have type
Type.{u+1} → Type.{u+1} → Type.{u}
/Users/5HT/depot/groupoid/exe/prelude/lean/TypeEqu.lean:15:25: error: unknown identifier 'Setoid'
TypeEqu.{l_1} : Type.{l_1+1} → Type.{l_1+1} → Type.{l_1}
[2/6] "/usr/local/Cellar/lean/" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/Mor.ilean"
ninja: build stopped: subcommand failed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.