| open import 1Lab.Type | |
| open import 1Lab.Path | |
| open import 1Lab.Path.Groupoid | |
| open import Data.Bool | |
| data Niltok : Type where | |
| t : Niltok | |
| nicht : Niltok → Niltok | |
| mod2 : (n : Niltok) → n ≡ nicht (nicht n) | |
| coh : (n : Niltok) → ap nicht (mod2 n) ≡ mod2 (nicht n) |
| Function Remove-DupDownloads { | |
| param ( | |
| [string]$SearchPath = ".", | |
| [switch]$Recurse = $false | |
| ) | |
| $FilePattern = '.*\([1-9][0-9]*\).*' | |
| $GCIParams = @{ | |
| 'Path' = $SearchPath | |
| 'File' = $true |
Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.
I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there
| open import Agda.Builtin.Equality | |
| -- Some familiar results about equality | |
| UIP : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q | |
| UIP x y refl refl = refl | |
| coerce : {A : Set} (B : A → Set) | |
| → {x y : A} → x ≡ y | |
| → B x → B y |
| ` ------------------------------------------------ | |
| ` Kevin Carlson, Astra Kolomatskaia, Reed Mullanix | |
| ` Narya formalisation of Kan complexes | |
| ` | |
| ` developed 13-18 May 2024 during the | |
| ` Prospects of Formal Mathematics | |
| ` trimester program at the | |
| ` Hausdorff Institute for Mathematics | |
| ` | |
| ` dated 7 June 2024 |
