Zulip Chat Archive

Stream: general

Topic: How to choose between prop and type?

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