Peculiar error

Stream: general

[Mai]

I managed to trigger a peculiar error, any help? :sweat_smile:

structure PosVar where
  n : Nat
  level : Nat

inductive Any (a : Type) where
  | func : List a -> Any a -> Any a
  | var : PosVar -> Any a

def Any.level : Any a -> Nat
  | .func _ _ => 9999999
  | .var v => v.level

inductive Precondition where
  | isFunc : (f : PosVar) -> (dom : Any Precondition) -> (codom : PosVar) ->
    {_ : dom.level <= f.level} -> {_ : codom.level <= f.level} -> Precondition

[Mai]

(kernel) application type mismatch
  Any.level Precondition dom
argument has type
  _nested.Any_1
but function has type
  Any Precondition → Nat

[Aaron Liu]

You can't use the recursive function Any.level on (dom : Any Precondition) since it recursively mentions the inductive definition being defined.

[Mai]

I see

[Mai]

I am not quite sure where would be the best place to store the proofs then