{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ProvingBasics where

Agda 作為證明語言#

import Padova2025-zh-TW.ProvingBasics.PropositionsAsTypes
import Padova2025-zh-TW.ProvingBasics.EvenOdd
import Padova2025-zh-TW.ProvingBasics.Negation
import Padova2025-zh-TW.ProvingBasics.Equality
import Padova2025-zh-TW.ProvingBasics.Connectives
import Padova2025-zh-TW.ProvingBasics.Termination