search

leanprover-community / lean-perfectoid-spaces

Perfectoid spaces in the Lean formal theorem prover.
https://leanprover-community.github.io/lean-perfectoid-spaces/
Apache License 2.0
115 stars 13 forks source link

Project does not currently compile #30

Closed kbuzzard closed 5 years ago

kbuzzard commented 5 years ago

Following the cut-n-paste installation instructions on master gives a repo which does not complile. We have not updated mathlib for a while, and Patrick and I have between us managed to create two non-rfl instances of a class. 

/home/buzzard/lean-projects/lean-perfectoid-spaces/src/r_o_d_completion.lean:43:2: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  domain.to_ring (ring_completion (valuation_field (out (v.val))))
inferred
  comm_ring.to_ring (ring_completion (valuation_field (out (v.val))))
PatrickMassot commented 5 years ago

This description is not accurate, those instances are defeq:

import algebra.field

example (α : Type*) [discrete_field α] :  @domain.to_ring α _  = @comm_ring.to_ring α _  := rfl

I really don't know what Lean is doing here. It seems this error message happens at a time where defeq is not good enough. It would be nice to be able to minimize this issue.

PatrickMassot commented 5 years ago

This issue is completely outdated.