Skip to content

Instantly share code, notes, and snippets.

import Lean
opaque g (n : Nat) : Nat
@[simp] def f (i n m : Nat) :=
if i < n then
f (i+1) n (g m)
else
m
termination_by n - i
@AndrasKovacs
AndrasKovacs / CCCNbE.agda
Last active March 17, 2021 18:11
NbE for CCC
open import Data.Unit
open import Data.Product
infixr 4 _⇒_ _*_ ⟨_,_⟩ _∘_
data Obj : Set where
∙ : Obj
base : Obj
_*_ : Obj → Obj → Obj
@henrytill
henrytill / landins_knot.ml
Created March 28, 2017 20:53
Landin's Knot
(** "Landin's Knot" - implements recursion by backpatching *)
let landins_knot f =
let r = ref (fun x -> assert false) in
let fixedpoint = f (fun x -> !r x) in
r := fixedpoint;
fixedpoint
let factorial =
let g f x =
if x = 0 then
@Earnestly
Earnestly / c99_ub_list.rst
Last active September 27, 2024 22:10
C99 List of Undefined Behavior (193 Cases)

C99 List of Undefined Behavior

From N1256: (See http://port70.net/~nsz/c/c99/n1256.html#J.2)

  • A "shall" or "shall not" requirement that appears outside of a constraint is violated (clause 4).
  • A nonempty source file does not end in a new-line character which is not immediately preceded by a backslash character or ends in a partial preprocessing token or comment (5.1.1.2).
  • Token concatenation produces a character sequence matching the syntax of a universal character name (5.1.1.2).
  • A program in a hosted environment does not define a function named main using one of the specified forms (5.1.2.2.1).
  • A character not in the basic source character set is encountered in a source file, except in an identifier, a character constant, a string literal, a header name, a comment, or a preprocessing token that is never converted to a token (5.2.1).
  • An identifier, comment, string literal, character constant, or header name contains an invalid multibyte character or does not
@jcmckeown
jcmckeown / IRExample.v
Created January 15, 2015 23:59
coq very nearly has induction-recursion
(**
Dybjer and Setzer provide a logical framework in which Induction-Recursion —
mutual definition of an (A : Type) and a (B : A -> V), in which constructors for A can talk about values of B, and B is defined by case analysis on members of A —
becomes equivalent to supposing initial algebras for certain functors on { X : Set & X -> V }. However, this latter family is, up to equivalences over V, the same as ordinary maps V -> Set. The universal case, in which V = Set, becomes somewhat trickier, for universe level reasons.
In any case, here is one way to define a "large" universe ("large" in the sense: we allow all externally definable functions) with naturals, dependent sums, and dependent products. A more careful presentation might work on a fibration over functions,
{ AB : Type * Type & fst AB -> snd AB } -> Type
instead, but good luck with that.
*)
@pix
pix / Makefile
Created May 12, 2011 15:20
delete-null-pointer-checks
all:
@echo "gcc-4.4 && -fdelete-null-pointer-checks"
@gcc-4.4 -O2 -ggdb -Wall -Wundef -fno-strict-aliasing -fno-common -fdelete-null-pointer-checks test-deref.c -o test-deref
@./test-deref || true &&
@echo "gcc-4.5 && -fdelete-null-pointer-checks"
@gcc-4.5 -O2 -ggdb -Wall -Wundef -fno-strict-aliasing -fno-common -fdelete-null-pointer-checks test-deref.c -o test-deref
@./test-deref || true
@echo "gcc-4.4 && -fno-delete-null-pointer-checks"
@gcc-4.4 -O2 -ggdb -Wall -Wundef -fno-strict-aliasing -fno-common -fno-delete-null-pointer-checks test-deref.c -o test-deref
@./test-deref || true