diff options
author | stuebinm | 2022-06-29 01:28:53 +0200 |
---|---|---|
committer | stuebinm | 2022-06-29 01:28:53 +0200 |
commit | 4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d (patch) | |
tree | 2819976f3fe60d2e9796ec37d2b0736df55daa59 /HoTT_Typing.thy | |
parent | cb4139dc35527bd8c8f9b70753c3d1f552c5f19d (diff) |
this just replaces all instance of `this` with instances of `infer`.
Unfortunately, it looks likes something else also broke, and I have
no idea what it is (but the proof for equiv_if_equal fails).
Sadly this means we can't get to univalence for now …
(but rn I'm too tired to try anything else with it)
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions