fork download

copy

-- proof for a /\ b is a pair of proofs for a and b
data _/\_ (a : Set) (b : Set) : Set where
	and : a -> b -> (a /\ b)
 
-- proof of equivalence is a pair of proofs for implications
data _<->_ (a : Set) (b : Set) : Set where
	eq : ((a -> b) /\ (b -> a)) -> (a <-> b)
 
-- composition of proofs
_._ : {a b c : Set} -> (b -> c) -> (a -> b) -> (a -> c)
_._ f g x = f (g x)
 
-- proofs in both directions are generated as composition of implication proofs 
proof : {p q r : Set} -> ((p <-> q) /\ (q <-> r)) -> (p <-> r)
proof (and (eq (and pq qp)) (eq (and qr rq))) = eq (and (qr . pq) (qp . rq))

prog.cpp:1:1: error: stray '\' in program
 -- proof for a /\ b is a pair of proofs for a and b
 ^
prog.cpp:2:1: error: stray '\' in program
 data _/\_ (a : Set) (b : Set) : Set where
 ^
prog.cpp:3:2: error: stray '\' in program
  and : a -> b -> (a /\ b)
  ^
prog.cpp:7:2: error: stray '\' in program
  eq : ((a -> b) /\ (b -> a)) -> (a <-> b)
  ^
prog.cpp:14:1: error: stray '\' in program
 proof : ((p <-> q) /\ (q <-> r)) -> (p <-> r)
 ^
prog.cpp:1:1: error: expected unqualified-id before '--' token
 -- proof for a /\ b is a pair of proofs for a and b
 ^
prog.cpp:10:21: error: expected unqualified-id before '->' token
 _._ : {a b c : Set} -> (b -> c) -> (a -> b) -> (a -> c)
                     ^

Standard output is empty