e473c2e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Exists naming

commite473c2e26ed489970f7571f36b6566424e26b11c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 18 Nov 2011, 13:56 (15 years ago) parente713a98

3 files changed+9−9

unifiedsplit

lib/builtins.idr+6−6

@@ -1,11 +1,11 @@

1−data Sigma : (a : Set) -> (P : a -> Set) -> Set where

2− Exists : {P : a -> Set} -> (x : a) -> P x -> Sigma a P;

1+data Exists : (a : Set) -> (P : a -> Set) -> Set where

2+ Ex_intro : {P : a -> Set} -> (x : a) -> P x -> Exists a P;

4−getWitness : {P : a -> Set} -> Sigma a P -> a;

5−getWitness (Exists a v) = a;

4+getWitness : {P : a -> Set} -> Exists a P -> a;

5+getWitness (a ** v) = a;

7−getProof : {P : a -> Set} -> (s : Sigma a P) -> P (getWitness s);

8−getProof (Exists a v) = v;

7+getProof : {P : a -> Set} -> (s : Exists a P) -> P (getWitness s);

8+getProof (a ** v) = v;

1010FalseElim : _|_ -> a;

1111

src/Core/Elaborate.hs+1−1

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

1−{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}

33{- A high level language of tactic composition, for building

44 elaborators from a high level language into the core theory.

src/Idris/AbsSyntax.hs+2−2

@@ -610,8 +610,8 @@ eqDecl = PDatadecl eqTy (piBind [(n "a", PSet), (n "b", PSet),

610610 where n a = MN 0 a

611611

612612-- Defined in builtins.idr

613−sigmaTy = UN "Sigma"

614−existsCon = UN "Exists"

613+sigmaTy = UN "Exists"

614+existsCon = UN "Ex_intro"

615615

616616piBind :: [(Name, PTerm)] -> PTerm -> PTerm

617617piBind [] t = t