Erika Su (Dec 26 2022 at 14:59):
inductive Palindrome : List α → /- Prop or Type -/ where | nil : Palindrome  | single : (a : α) → Palindrome [a] | sandwich : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a])
Prop is useful for proving, but Type is also useful as it provides a "View" of List
(I learned this concept in type driven development in idris).
If it's only about proving then prop should be used. But it's also possible i need to give a computable function using view.
I don't think define two version (Prop and Type) of this inductive type is good practice, but i am also worried that using the latter will affect performance of the program when only type check is needed.
What's the best practice?
Last updated: Aug 03 2023 at 10:10 UTC