File: test-mjp.ott

package info (click to toggle)
ott 0.32%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 6,420 kB
  • sloc: ml: 25,065; makefile: 1,393; awk: 736; lisp: 183; sh: 14; sed: 4
file content (15 lines) | stat: -rw-r--r-- 289 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
embed 
{{ coq
Parameter heap : Set.
}}

metavar h ::= {{ coq heap }}

grammar
  s :: '' ::= 		       {{ coq prod (prod heap  heap) heap }}
    | ( h1 , h2 , h3 )	::  :: state  {{ coq ([[h1]],[[h2]],[[h3]]) }} 

  A, R :: '' ::= {{ com abstract command }} 
	{{ coq s_ty * s_ty -> bool }}