| class Fintype (α : Type) where | |
| axiom Finset (α : Type) : Type | |
| axiom Finset.univ {α : Type} [Fintype α] : Finset α | |
| axiom Finset.filter {α : Type} (s : Finset α) (ϕ : α → Bool) : Finset α | |
| -- The following should not elaborate, since there are no `Fintype` instances | |
| -- Instead it yields: "error: (kernel) declaration has metavariables 'kernelErrorMetavar'" | |
| def kernelErrorMetavar1 (n : Nat) : Finset (Fin n) := | |
| Finset.univ.filter (fun (i : Fin n) => true) | |
| instance : Fintype (Fin n) := ⟨⟩ | |
| noncomputable def kernelErrorMetavar2 (n : Nat) : Finset (Fin n) := | |
| Finset.univ.filter (fun (i : Fin n) => true) |