Abhishek Anand aa755

aa755 / diff

Last active June 25, 2024 14:07

aac_tactics do not anymore throw despite try

	coq@99313f5cc7b0:~/aac-tactics$ git log --stat
	commit 8ba7a8b2c5ce80859e9645c89ebe39c33948525c (HEAD -> master, origin/master, origin/HEAD)
	Author: Karl Palmskog <[email protected]>
	Date: Fri Jun 21 00:04:44 2024 +0200

	silence warning 67 in Dune build

	src/dune \| 2 +-
	1 file changed, 1 insertion(+), 1 deletion(-)

aa755 / gist:3bce323f3a3a93b6ddbf8bcee5d5a613

Created May 18, 2024 14:03

quotients as indices of inductives seems sound

	Axiom natMod7: Type.
	Axiom inj : nat -> natMod7.

	Inductive Vector : natMod7 → Prop :=
	\| ttrue : Vector (inj 0)
	\| ffalse : False -> Vector (inj 7).

	Lemma eqq: inj 7 = inj 0. Proof. Admitted.

	Lemma ff: False.

aa755 / rewrite_drops_hyps.v

Last active October 11, 2022 20:12 — forked from Blaisorblade/rewrite_drops_hyps.v

Demonstrate strange rewrite behavior

aa755 / fplbill.v

Created September 8, 2022 21:05

fpl bill algorithm

	(** tries to reverse engineer FPL billing algorithm: given x watt consumption what should be the bill?
	the bill is printed in cents.
	it comes within 100cents in the test cases
	but doesnt exactly match, even though all computations except the last one to print in decimal (error < 1 cent) are exact.
	*)

	Require Import QArith.
	Require Import Coq.Classes.DecidableClass.
	Definition Qmax (a b:Q) : Q :=
	if ((Qle_bool a b)) then b else a.

aa755 / gist:f7be3bf8116930fd935251a1650633ff

Last active July 6, 2021 16:26

Ivermectin factcheck rebuttal

moved to https://aa755.github.io/decoding-human-body/ivermectin/2021/07/05/ivmrebuttal.html