diff options
Diffstat (limited to 'docs/core-spec/OpSem.ott')
| -rw-r--r-- | docs/core-spec/OpSem.ott | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott index efed85a5f5..389c5e8106 100644 --- a/docs/core-spec/OpSem.ott +++ b/docs/core-spec/OpSem.ott @@ -45,8 +45,14 @@ not e2 is_a_coercion ----------------------------------------------- :: Push ((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0) ----------------------------------------- :: TPush -((\n.e) |> g) t --> (\n.(e |> g n)) t +% g : (forall (a : k1). t1) ~Rep# (forall (a : k2). t2) +% t : k2 +% g' : k2 ~# k1 +% t' : k1 +g' = sym (nth Nom 0 g) +t' = t |> g' +-------------------------------------------------------- :: TPush +((\n.e) |> g) t --> ((\n.e) t') |> (g @ (<t>_Nom |> g')) % g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6) % g2 : t3 ~Rep# t6 |