Naïm Camille Favier
Naïm Camille Favier
Bump nixpkgs to get [highlighting for `opaque` and `unfolding` keywords](https://invent.kde.org/frameworks/syntax-highlighting/-/merge_requests/726) in `--skip-agda` builds. Other notable changes: - `node2nix` [seems to be deprecated](https://github.com/NixOS/nixpkgs/issues/229475) and started failing, so I replaced it with...
Proposition 4.8.7 characterises the decidable predicates p : Pred(S) as those for which there is a decision procedure d : ∥S∥ → bool that takes a realiser for x to...
I got slightly confused by the following claims: https://github.com/andrejbauer/notes-on-realizability/blob/8dccd94381ec3bb343aa68ceed74b47b880ace32/notes/models.tex#L2161 https://github.com/andrejbauer/notes-on-realizability/blob/8dccd94381ec3bb343aa68ceed74b47b880ace32/notes/models.tex#L2367-L2371 Together with https://github.com/andrejbauer/notes-on-realizability/blob/8dccd94381ec3bb343aa68ceed74b47b880ace32/notes/introduction.tex#L99-L101 they seem to imply that the Ackermann function is not definable in Gödel's system T, or in...
Fixes https://github.com/andrejbauer/notes-on-realizability/issues/18 This just pulls the files from the current master branch of kaobook, https://github.com/fmarotta/kaobook/commit/23dbe706534aba4b1a6e8b07a6fd364cde5c9307, which includes the fix for https://github.com/fmarotta/kaobook/issues/155. The latest release of kaobook is from June 2021...
The PDF table of contents, displayed in the sidebar in e.g. Firefox or Evince, is broken: (click for a screenshot)  EDIT: This is a known kaobook issue (https://github.com/fmarotta/kaobook/issues/155) that...
Fīxes https://github.com/NixOS/nixos-hardware/issues/1603 for Framework 13 AMD AI series laptops. ###### Things done - [X] Tested the changes in your own NixOS Configuration - [X] Tested the changes end-to-end by using...