Modus ponens

Description

Prove 'Modus ponens'.

Theorem (download)

module Theorem where

import Level

postulate
  modus-ponens : ∀ {a b} {P : Set a} {Q : Set b} → (P → Q) → P → Q

Verifier

module Verifier where

open import Theorem

verify : ∀ {a b} {P : Set a} {Q : Set b} → (P → Q) → P → Q
verify = modus-ponens

Proofs

Rank Prover Size Date
1 strout 52 2014-01-06 10:52:31 JST
2 Rotsor 62 2013-12-28 23:30:09 JST
3 kdxu 88 2014-03-16 16:17:52 JST
4 cutsea110 88 2013-05-28 10:29:10 JST
5 phi16_ 90 2017-11-14 15:35:28 JST
6 masahiro_sakai 90 2014-11-25 00:20:02 JST
7 trigott 90 2014-04-15 23:53:32 JST
8 kiritex 90 2014-04-04 16:01:09 JST
9 chiguri 90 2013-05-28 12:53:59 JST
10 Lost_dog_ 90 2013-05-27 09:42:11 JST
11 nrolland 92 2014-12-26 00:34:38 JST
12 notogawa 106 2013-05-26 00:35:12 JST
13 ikegami__ 200 2013-10-16 11:58:12 JST