Alex Rozanov hacklex

hacklex / SimpleAlgebraTactics.fst

Created March 30, 2025 14:21

Simple tactic to prove associativity in setoid monoids

	module SimpleAlgebraTactics

	open FStar.Tactics.V2
	open FStar.List
	open FStar.List.Tot

	noeq type setoid_monoid (a: Type) = {
	eq: a -> a -> Type; (* Equivalence relation *)
	op: a -> a -> a;
	id: a; (* Identity element *)

hacklex / MinimalApplyLemmaBugReproduction.fst

Created April 6, 2025 16:25

Calling lemma via apply_lemma fails in manual case (line 115)

	module MinimalApplyLemmaBugReproduction

	open FStar.Tactics.V2
	open FStar.List
	open FStar.List.Tot

	noeq type setoid_monoid (a: Type) = {
	eq: a -> a -> Type;
	op: a -> a -> a;
	id: a;