Agda命题逻辑(0) 目录

{-# OPTIONS --without-K --safe #-}

module Everything where

(1) 希尔伯特系统

open import Hilbert public

(2) 演绎定理

open import Deduction public