🎇

Sewon Park park-sewon

🎇

park-sewon / IntuitionisticAttr.lean

Created March 2, 2025 16:28

LEAN tag attribute for checking classical axioms in Prop

	import Lean
	import Lean.Util.CollectAxioms
	open Lean

	initialize intuitionisticAttr : TagAttribute ←
	registerTagAttribute `intuitionistic "Tag attribute for intuitionistic prop"
	fun decl =>
	do
	let axioms ← collectAxioms decl
	let invalid_axioms := axioms.filter

park-sewon / practice_coq_1.v

Created April 16, 2023 09:32

A simple Coq practice session

	(* Context와 state가 있는 프로그래밍 언어를 정형화하고자 합니다.
	프로그래밍 변수로는 De Brujin index를 사용할 것이며,
	따라서 context는 단순히 데이터 타입들의 리스트 입니다.
	(예를 들어서 int :: int :: boolean :: nil 이 하나의 context입니다.
	리스트를 사용해서 생기는 문제를 해결해 봅시다.

	16 April 2023 -- Sewon Park *)

	Require Import List.