Zulip Chat Archive

Stream: maths

Topic: Type expected error


view this post on Zulip Ashvni Narayanan (Feb 26 2021 at 12:12):

I am trying to define dir_sys as the following : a collection of finite sets (X_i)_{i ∈ ℕ} such that for j ≤ i, there exists a surjective map π_{ij} such that for k ≤ j ≤ i, π_{ij} ∘ π_{jk} = π_{ik}. I get stuck here:

import ring_theory.int.basic
import set_theory.zfc

structure dir_sys :=
( α : Type* )
(h :   finset α )
(sys :  i j : , j  i   f : (h i).1  (h j).1, function.surjective f )

The error I get is :

type expected at
  (h i).val
term has type
  quot setoid.r

I don't understand the error. Does Lean want me to specify the type of (h i).val? Any help is appreciated, thank you!

view this post on Zulip Eric Wieser (Feb 26 2021 at 12:15):

Adding an explicit might help

view this post on Zulip Eric Wieser (Feb 26 2021 at 12:15):

↥(h i).1 → ↥(h j).1 or similar

view this post on Zulip Eric Wieser (Feb 26 2021 at 12:15):

Why the .1 which turns your finset into a multiset?

view this post on Zulip Ashvni Narayanan (Feb 26 2021 at 12:21):

Eric Wieser said:

Adding an explicit might help

I get the following error :

type expected at
  (h i)
term has type
  has_coe_to_sort.S (finset α)

view this post on Zulip Ashvni Narayanan (Feb 26 2021 at 12:21):

Eric Wieser said:

Why the .1 which turns your finset into a multiset?

I was just experimenting..

view this post on Zulip Kevin Buzzard (Feb 26 2021 at 12:37):

My instinct is that we might already have some far more general kind of directed systems in mathlib already. I think that the functions themselves should be part of the data, not just some assumption that they exist. Might it be easier to work with types rather than finsets, which are terms?

view this post on Zulip Eric Wieser (Feb 26 2021 at 12:40):

We have docs#direct_limit which seems to have some things in common with what you're after

view this post on Zulip Eric Wieser (Feb 26 2021 at 12:42):

This works:

import data.finset.basic

structure dir_sys :=
( α : Type* )
(h :   finset α )
(sys :  i j : , j  i   f : (h i : set α)  (h j : set α), function.surjective f )

view this post on Zulip Eric Wieser (Feb 26 2021 at 12:42):

finset has no coercion to sort

view this post on Zulip Eric Wieser (Feb 26 2021 at 12:42):

Only coercion to set, which then has a coercion to sort


Last updated: May 18 2021 at 06:15 UTC