4 ms·
Actually, AFAIU, you can define simple inductive types via church literals. However, you can't define induction principle for them. However, without induction p
by solomatov 12y ago
Actually, AFAIU, you can define simple inductive types via church literals. However, you can't define induction principle for them. However, without induction principles, you can't prove anything useful.
- mafribe 12y agoYou can define induction, but you can't prove it, you need to introduce it as an assumption. That's inconvenient.
- solomatov 12y agoYou can define induction operator, but it won't have required type.
- llcv 12y agoCan you explain further?
- solomatov 12y agoFor example, let's see how to define induction principle for Nat. We should define two terms with the following types: NatRec : (R : Set) -> R -> (R -> R) -> Nat -> R NatInd : (C : Nat -> Set) -> (C zero) -> ((n : Nat) -> C n -> C (suc n)) -> (n : Nat) -> (C n) For the first we can represent zero and suc as functions of the first type (it will be church literals). However, we can't do the same for the second. We can create a term which has that type but it won't typecheck.