| Parents |
| gst |
| Constants |
|
instantiate
|
(GS  GS) GS GS
|
|
$
 gp |
GS GS BOOL
|
|
$p
|
GS GS GS
|
|
elaborate
|
(GS GS) GS BOOL
|
|
$
gd |
GS GS BOOL
|
| Fixity |
| Right Infix 230: |
gd |
gp |
Right Infix 240: |
p |
| Definitions |
|
instantiate
|
 ConstSpec  ( instantiate'   f s instantiate' f (Unit s) = Imagep (instantiate' f) s  ( ( t s = Unit t)  instantiate' f s = f s)) instantiate
|
|
gp |
s t s gp t  ( f s = instantiate f t)
|
|
p
|
f x f p x = ( y x  g y gp f)
|
|
elaborate
|
ConstSpec ( elaborate' f s t v elaborate' f ( g g s g t) instantiate f s = instantiate f t elaborate' f (Unit g g s g t) instantiate f s g instantiate f t elaborate' f (Pair (Unit g) g g v g s g t) ( x (let f' y = (if y = v then x else f y) in elaborate' f' s elaborate' f' t))) elaborate
|
|
gd |
s t s gd t elaborate ( v s) t
|
