File: bug_19082.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 (25 lines) | stat: -rw-r--r-- 469 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
20
21
22
23
24
25
 
Inductive boring1 := Boring1.
Inductive boring2 := Boring2.

Inductive output_wrapper := OutputWrapper {
    ow_alice : boring1;
}.

#[projections(primitive)]
Inductive request := InputWrapper {
    req_alice : boring1;
    req_next_bob := Boring2;
}.

Definition do_the_thing (req : request) : output_wrapper.
Proof.
  exact (
      match req with
      | {|
          req_alice := alice;
       |} =>
        OutputWrapper alice
      end
  ).
  Validate Proof.
Qed.