How to choose between prop and type/view ?

Stream: general

[Henrik Böving]

We would usually define Palindrom as List a -> Prop and if you want to use the fact that some list is a palindrom use a Subtype

[Trebor Huang]

The more Lean-y way is to use something like

inductive View (l : List a) : Type where
  even : (half : List a) ... l is made from half ... -> View l
  odd : ... similar

[Trebor Huang]

This way actually more code is reused, and the Idris style views are less beneficial because we have powerful automation.

[Trebor Huang]

You can see the same style difference just from how we define Fin.