O que significa apagar um argumento em um construtor de tipo? Por exemplo
data Foo : (0 _ : Nat) -> Type where
em oposição a
data Foo : Nat -> Type where
Meu entendimento é que nada em um construtor de tipo é usado em tempo de execução, então é sempre 0. Acho que isso também leva à questão talvez mais confusa do que significaria um argumento linear em um construtor de tipo, mas isso fica para outro dia.