Skip to content

Instantly share code, notes, and snippets.

@5HT

5HT/gist:02083fb79b0ca32fffff

Created February 14, 2016 08:22
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save 5HT/02083fb79b0ca32fffff to your computer and use it in GitHub Desktop.
Save 5HT/02083fb79b0ca32fffff to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
$ 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