e473c2e · Idris-dev · git.iko.soy

lib/builtins.idr+6−6

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

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

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

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

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

3

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

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

5−getWitness (Exists a v) = a;

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

6

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

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

8−getProof (Exists a v) = v;

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

9

10FalseElim : _|_ -> a;

11

src/Core/Elaborate.hs+1−1

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

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

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

2

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

4 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),

610 where n a = MN 0 a

611

612-- Defined in builtins.idr

613−sigmaTy = UN "Sigma"

613+sigmaTy = UN "Exists"

614−existsCon = UN "Exists"

614+existsCon = UN "Ex_intro"

615

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

617piBind [] t = t