git.iko.soy/Idris-dev
on master help sign in
Make evidence witness explicit.
b9781fbMatus Tejiscak
libs/prelude/Prelude/Pairs.idr+3−3
compare with master
unifiedsplit
@@ -9,7 +9,7 @@ using (a : Type, P : a -> Type)
9
9
10 ||| Dependent pair where the first field is erased.
10 ||| Dependent pair where the first field is erased.
11 data Exists : (P : a -> Type) -> Type where
11 data Exists : (P : a -> Type) -> Type where
12− evidence : .{x : a} -> (pf : P x) -> Exists P
12+ evidence : .(x : a) -> (pf : P x) -> Exists P
13
13
14 ||| Dependent pair where the second field is erased.
14 ||| Dependent pair where the second field is erased.
15 data Subset : (a : Type) -> (P : a -> Type) -> Type where
15 data Subset : (a : Type) -> (P : a -> Type) -> Type where
@@ -25,8 +25,8 @@ using (a : Type, P : a -> Type)
25 getProof : (x : T) -> P (getWitness x)
25 getProof : (x : T) -> P (getWitness x)
26
26
27 instance DepPair a P (Exists {a} P) where
27 instance DepPair a P (Exists {a} P) where
28− getWitness (evidence {x=x} pf) = x
28+ getWitness (evidence x pf) = x
29− getProof (evidence {x=x} pf) = pf
29+ getProof (evidence x pf) = pf
30
30
31 instance DepPair a P (Subset a P) where
31 instance DepPair a P (Subset a P) where
32 getWitness (element x pf) = x
32 getWitness (element x pf) = x
test/basic010/Main.idr+2−2
@@ -5,8 +5,8 @@ qib Z = 1
5qib (S Z) = 1
5qib (S Z) = 1
6qib (S (S n)) = qib n * qib (S n)
6qib (S (S n)) = qib n * qib (S n)
7
7
8−f : (n : Nat) -> Exists (\k => qib n = k)
8+f : (n : Nat) -> Exists (\k : Nat => qib n = k)
9−f n = witness (qib n) refl
9+f n = evidence (qib n) refl
10
10
11main : IO ()
11main : IO ()
12main = print "hello world"
12main = print "hello world"
test/basic010/run+1
@@ -1,4 +1,5 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2+
2idris $@ Main.idr --nocolour --check --warnreach -o basic010
3idris $@ Main.idr --nocolour --check --warnreach -o basic010
3./basic010
4./basic010
4rm -f *.ibc basic010
5rm -f *.ibc basic010