File: bug_13271.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (19 lines) | stat: -rw-r--r-- 567 bytes parent folder | download | duplicates (2)
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.