зеркало из https://github.com/microsoft/ivy.git
19 строки
162 B
Plaintext
19 строки
162 B
Plaintext
|
#lang ivy1.7
|
||
|
|
|
||
|
|
type t
|
||
|
|
relation p(X:t)
|
||
|
|
|
||
|
|
schema foo = {
|
||
|
|
function v : t
|
||
|
|
property p(v)
|
||
|
|
}
|
||
|
|
|
||
|
|
var w : t
|
||
|
|
|
||
|
|
property [thing] p(w)
|
||
|
|
proof
|
||
|
|
assume foo with v = w
|
||
|
|
|
||
|
|
|
||
|
|
|