Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
$ linja
[2/6] "/usr/local/Cellar/lean/0.2.0.20151013125924.gitd508ceccecf8504...clean" -i "/Users/5HT/depot/groupoid/exe/prelude/lean/TypeEqu.ilean"
FAILED: "/usr/local/Cellar/lean/0.2.0.20151013125924.gitd508ceccecf8504257b538de57d3c76ad1e20b35/bin/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/0.2.0.20151013125924.gitd508ceccecf8504...Mor.clean" -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.