File: gmap2.ott

package info (click to toggle)
ott 0.34%2Bds-2
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 6,440 kB
  • sloc: ml: 25,103; makefile: 1,375; awk: 736; lisp: 183; sh: 14; sed: 4
file content (17 lines) | stat: -rw-r--r-- 367 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
 
embed 
{{ coq
From stdpp Require Import gmap.
}}
grammar
context :: context_ ::=
 {{ coq gmap nat nat }}
 {{ coq-universe Type }}
 {{ coq-notation }}
| [] :: M :: empty
  {{ coq GMap GEmpty }}
embed
{{ coq
Fact insert_lookup_ne_context: forall (C:context) i j x y,
    i <> j -> C !! i = Some x -> <[j:=y]> C !! i = Some x.
Proof. by intros; simplify_map_eq. Qed.
}}