b9781fb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make evidence witness explicit.

commitb9781fbd0996315afe9ba718671280e56b3ba40c authorMatus Tejiscak <ziman@functor.sk> dateWed 28 May 2014, 17:21 (12 years ago) parentf13c6ad

3 files changed+6−5

unifiedsplit

libs/prelude/Prelude/Pairs.idr+3−3

@@ -9,7 +9,7 @@ using (a : Type, P : a -> Type)

1010 ||| Dependent pair where the first field is erased.

1111 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

1313

1414 ||| Dependent pair where the second field is erased.

1515 data Subset : (a : Type) -> (P : a -> Type) -> Type where

@@ -25,8 +25,8 @@ using (a : Type, P : a -> Type)

2525 getProof : (x : T) -> P (getWitness x)

2626

2727 instance DepPair a P (Exists {a} P) where

28− getWitness (evidence {x=x} pf) = x

29− getProof (evidence {x=x} pf) = pf

28+ getWitness (evidence x pf) = x

29+ getProof (evidence x pf) = pf

3030

3131 instance DepPair a P (Subset a P) where

3232 getWitness (element x pf) = x

test/basic010/Main.idr+2−2

@@ -5,8 +5,8 @@ qib Z = 1

55qib (S Z) = 1

66qib (S (S n)) = qib n * qib (S n)

8−f : (n : Nat) -> Exists (\k => qib n = k)

9−f n = witness (qib n) refl

8+f : (n : Nat) -> Exists (\k : Nat => qib n = k)

9+f n = evidence (qib n) refl

1010

1111main : IO ()

1212main = print "hello world"

test/basic010/run+1

@@ -1,4 +1,5 @@

11#!/usr/bin/env bash

23idris $@ Main.idr --nocolour --check --warnreach -o basic010

34./basic010

45rm -f *.ibc basic010