git.iko.soy/Idris-dev
on master help sign in
Rename Pair to Sigma.
commit42c28d2e6348456270976b68fcdb8b519a268e91 authorMatus Tejiscak <ziman@functor.sk> dateThu 29 May 2014, 15:41 (12 years ago) parentbf4c0ed
4 files changed+11−11
compare with master
unifiedsplit
libs/prelude/Builtins.idr+2−2 libs/prelude/Prelude/Pairs.idr+5−5 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Delaborate.hs+2−2
libs/prelude/Builtins.idr+2−2
@@ -6,8 +6,8 @@
66||| Dependent pairs, in their internal representation
77||| @ a the type of the witness
88||| @ P the type of the proof
9−data Pair : (a : Type) -> (P : a -> Type) -> Type where
10− pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair a P
9+data Sigma : (a : Type) -> (P : a -> Type) -> Type where
10+ Sg_intro : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
1111
1212||| The eliminator for the empty type.
1313FalseElim : _|_ -> a
libs/prelude/Prelude/Pairs.idr+5−5
@@ -31,12 +31,12 @@ using (a : Type, P : a -> Type)
3131 getProof : (x : Subset a P) -> P (getWitness x)
3232 getProof (element x pf) = pf
3333
34− namespace Pair
35− getWitness : Pair a P -> a
36− getWitness (pair x pf) = x
34+ namespace Sigma
35+ getWitness : Sigma a P -> a
36+ getWitness (x ** pf) = x
3737
38− getProof : (x : Pair a P) -> P (getWitness x)
39− getProof (pair x pf) = pf
38+ getProof : (x : Sigma a P) -> P (getWitness x)
39+ getProof (x ** pf) = pf
4040
4141 -- Polymorphic (class-based) projections have been removed
4242 -- because type-directed name disambiguation works better.
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1098,8 +1098,8 @@ elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defau
10981098 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
10991099
11001100-- Defined in builtins.idr
1101−sigmaTy = sUN "Pair"
1102−existsCon = sUN "pair"
1101+sigmaTy = sUN "Sigma"
1102+existsCon = sUN "Sg_intro"
11031103
11041104piBind :: [(Name, PTerm)] -> PTerm -> PTerm
11051105piBind = piBindp expl
src/Idris/Delaborate.hs+2−2
@@ -92,13 +92,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
9292 | n == eqCon = PRefl un (de env [] r)
9393 | n == sUN "lazy" = de env [] r
9494 deFn env (P _ n _) [ty, Bind x (Lam _) r]
95− | n == sUN "Pair"
95+ | n == sUN "Sigma"
9696 = PDPair un IsType (PRef un x) (de env [] ty)
9797 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
9898 deFn env (P _ n _) [_,_,l,r]
9999 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
100100 | n == eqTy = PEq un (de env [] l) (de env [] r)
101− | n == sUN "pair" = PDPair un IsTerm (de env [] l) Placeholder
101+ | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder
102102 (de env [] r)
103103 deFn env f@(P _ n _) args
104104 | n `elem` map snd env