1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
|
Require Program.Tactics.
Definition PeanoWithMax (maxValue : nat) : Set := { value : nat | value <= maxValue }.
Polymorphic Definition NonEmptyList (elementType : Type) : Type :=
{ list : list elementType | list <> nil }.
Axiom n : nat.
Axiom ListFromPeano : forall (value : nat), list (PeanoWithMax n).
Polymorphic Program Definition FromPeano (value : nat) : NonEmptyList (PeanoWithMax n) :=
match value with
| 0 => exist _ (cons (exist _ 0 _) nil) _
| S _ => exist _ (ListFromPeano value) _
end.
Next Obligation.
Admitted.
Next Obligation.
Admitted.
|