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/Univalence.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 'hott/Univalence.thy')
0 files changed, 0 insertions, 0 deletions