park-sewon

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

Require Import List.

park-sewon

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