universe level of inductive type

Stream: lean4

[Jared green]

import Init.Data.List
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Join
import Mathlib.Data.Bool.Basic
open Classical

variable {a : Type} [h : DecidableEq a] {pred : a -> Prop}
inductive variadic a pred
  where
  | vatom : a -> (variadic a pred)
  | vAnd : List (variadic a pred) -> variadic a pred
  | vOr : List (variadic a pred)  -> variadic a pred
  | vNot : variadic a pred -> variadic a pred
deriving DecidableEq

[Marcus Rossel]

What's your question?

[Jared green]

its failing to compute the universe level of variadic, and i dont know why

[Eric Wieser]

This works:

inductive variadic (a : Type) [DecidableEq a] (pred : a -> Prop)
  where
  | vatom : a -> (variadic a pred)
  | vAnd : List (variadic a pred) -> variadic a pred
  | vOr : List (variadic a pred)  -> variadic a pred
  | vNot : variadic a pred -> variadic a pred

[Eric Wieser]

Your variable line is being ignored because inductive variadic a pred is defining brand new a and pred variables

[Eric Wieser]

You can see this by looking at the "Expected type" after the : on the line where the error message is, which is

a✝: Type
h: DecidableEq a✝
pred✝: a✝ → Prop
a: Sort u_1
pred: ?m.38 a
⊢ Type ?u.50

[Jared green]

i have another file where that doesnt happen. im not sure what the difference is

import Init.Data.List
import Init.PropLemmas
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
open Classical

variable {a : Type}[h: DacidableEq a]
inductive normalizable a (pred : a -> Prop)
  where
  | atom : a -> (normalizable a pred)
  | And : (normalizable a pred) -> (normalizable a pred) -> (normalizable a pred)
  | Or : (normalizable a pred) -> (normalizable a pred) -> (normalizable a pred)
  | Not : (normalizable a pred) -> (normalizable a pred)
deriving DecidableEq

[Mario Carneiro]

If you want a variable to be used , you should not put it in the binder list, i.e. you should just write inductive variadic where ... instead of inductive variadic a pred where .... When you use a binder in the declaration, it always creates a new variable, even if it happens to be shadowing an existing variable (in which case the first variable will not be used). Note that variadic will end up being defined with parameters for all the variables, even though in the declaration itself it will appear without being applied to the variables (i.e. you will write | vatom : a -> variadic but the resulting constructor will be variadic.vatom (a : Type) [DecidableEq a] (pred : a -> Prop) : a -> variadic a pred).

[Jared green]

so, in both files i need normalizable and variadic to depend on a and pred, and a needs decidable equality. when i had started implementing normalizable, a and pred was used as the dependency whenever the type ascription called for it, which is why i made it a variable. how would that be better implemented?

[Mario Carneiro]

Using a variable is fine, but you should not also use it as a binder name because that's shadowing the variable declaration

[Mario Carneiro]

concretely, I'm suggesting, for your two examples:

variable (a : Type) [DecidableEq a] (pred : a -> Prop)
inductive variadic
  where
  | vatom : a -> variadic
  | vAnd : List variadic -> variadic
  | vOr : List variadic  -> variadic
  | vNot : variadic -> variadic
deriving DecidableEq

variable (a : Type) [DecidableEq a]
inductive normalizable (pred : a -> Prop)
  where
  | atom : a -> (normalizable pred)
  | And : (normalizable pred) -> (normalizable pred) -> (normalizable pred)
  | Or : (normalizable pred) -> (normalizable pred) -> (normalizable pred)
  | Not : (normalizable pred) -> (normalizable pred)
deriving DecidableEq

[Jared green]

suppose i need the elements to have their atoms be uniform in their source type and pred, for both.