LizzyFleckenstein03

-- this program is GPLv3
-- Copyright (C) 2024 Charlotte Pabst aka Lizzy Fleckenstein

import Mathlib.Tactic.Linarith

--
-- Define correctness for sorting algorithms
--

-- list is sorted, i.e. no element is smaller than its predecessor

LizzyFleckenstein03

Require Import Arith Bool Combinators FinFun Lia List.
Import ListNotations.
Open Scope list_scope.
Open Scope nat.
Scheme Equality for list.

(* helpers missing in the standard library *)

Lemma NoDup_app {A : Type} (a b : list A) : NoDup a -> NoDup b -> (forall x, In x a -> ~(In x b)) -> NoDup (a ++ b).
Proof.

LizzyFleckenstein03

wgsl
\.wgsl$

LizzyFleckenstein03

/*
	This program demonstrates how unnamed anonymous struct/union fields get embedded in C.

	License: CC BY-SA 4.0
*/

typedef struct {
	int age;
	struct {
		char *name;

LizzyFleckenstein03

/*
	If -Wpedantic is enabled, casts between function pointers and void* are forbidden.
	("ISO C forbids conversion of function pointer to object pointer type")
	However, a function pointer can be wrapped in a struct, a pointer to which can in turn be casted to void*.

	This program demonstrates how this trick can be abused to cause undefined behavior.

	Build: cc -Wall -Wextra -Wpedantic -Werror callback.c -o callback
	Run: ./callback