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

park-sewon

section Acc_from_Coq

  variable {P : Nat → Prop}

  inductive Proof : Prop → Type where
  | proof : Q -> Proof Q

  variable {P_dec : ∀ n, (Proof (P n)) ⊕ (Proof (¬ (P n)))}

  abbrev R (x y : Nat) : Prop := x = y + 1 ∧ ¬ P y

park-sewon

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

Require Import List.