Changed header anchors. Commited WIP fix for #577.

This commit is contained in:
Wen Kokke 2021-08-25 11:53:30 +01:00
parent 07d082c9db
commit a5e1f77d22
No known key found for this signature in database
GPG key ID: 7EB7DBBCEB539DB8
2 changed files with 33 additions and 2 deletions

View file

@ -0,0 +1,31 @@
local chapter = nil
function Header(el)
if el.level == 2 then
chapter = el.attr.identifier
end
if el.level >= 3 then
if el.attr.attributes.name then
el.attr.identifier = chapter .. '-' .. el.attr.attributes.name
el.attr.attributes.name = nil
else
el.attr.identifier = chapter .. '-' .. el.attr.identifier
end
end
end
function show(t)
local str = ''
str = str .. '{'
for k,v in pairs(t) do
str = str .. k
str = str .. ':'
if type(v) == 'table' then
str = str .. show(v)
else
str = str .. v
end
end
str = str .. '}'
return str
end

View file

@ -879,7 +879,7 @@ typed (C-suc c) = ⊢suc (typed c)
typed (C-rcd ⊢Ms dks As<:Bs) = <: (rcd Ms dks) As<:Bs
```
## Progress <a #"subtyping-progress"></a>
## Progress {#subtyping-progress}
The Progress theorem states that a well-typed term may either take a
reduction step or it is already a value. The proof of Progress is like
@ -952,7 +952,7 @@ progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M
* Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`.
## Preservation <a #"subtyping-preservation"></a>
## Preservation {#subtyping-preservation}
In this section we prove that when a well-typed term takes a reduction
step, the result is another well-typed term with the same type.