File tree Expand file tree Collapse file tree 1 file changed +0
-48
lines changed
Expand file tree Collapse file tree 1 file changed +0
-48
lines changed Original file line number Diff line number Diff line change 3434 ],
3535 "description" : " Loop invariant"
3636 },
37- "Method" : {
38- "prefix" : " method" ,
39- "body" : [
40- " method ${1:foo}(${2}) returns ${5:(res:Int)}" ,
41- " \t requires ${3:true}" ,
42- " \t ensures ${4:true}" ,
43- " {" ,
44- " \t ${6:assert true}" ,
45- " }"
46- ],
47- "description" : " Method"
48- },
49- "Predicate" : {
50- "prefix" : " predicate" ,
51- "body" : [
52- " predicate ${1:foo}(${2:xs:Ref})" ,
53- " {" ,
54- " \t ${3:acc(xs.next)}" ,
55- " }"
56- ],
57- "description" : " Predicate"
58- },
59- "Function" : {
60- "prefix" : " function" ,
61- "body" : [
62- " function ${1:foo}(${2:x:Int}): ${3:Bool}" ,
63- " \t requires ${4:true}" ,
64- " \t ensures ${5:true}" ,
65- " {" ,
66- " \t ${6}" ,
67- " }"
68- ],
69- "description" : " Function"
70- },
71- "Domain" : {
72- "prefix" : " domain" ,
73- "body" : [
74- " domain ${1:MyType[T]} {" ,
75- " \t function ${2:oper(m:MyType[T])}: ${3:Bool}" ,
76- " \t axiom ${4:ax_MyType} {" ,
77- " \t\t forall ${5:m:MyType[T]} :: " ,
78- " \t\t\t { ${6:oper(m)} }" ,
79- " \t\t\t\t ${7:oper(m) == true}" ,
80- " \t }" ,
81- " }"
82- ],
83- "description" : " Domain"
84- },
8537 "Axiom" : {
8638 "prefix" : " axiom" ,
8739 "body" : [
You can’t perform that action at this time.
0 commit comments