git.iko.soy/Idris-dev
on master help sign in
Rename Pair to Sigma.
42c28d2Matus Tejiscak
libs/prelude/Builtins.idr+2−2
compare with master
unifiedsplit
@@ -6,8 +6,8 @@
6||| Dependent pairs, in their internal representation
6||| Dependent pairs, in their internal representation
7||| @ a the type of the witness
7||| @ a the type of the witness
8||| @ P the type of the proof
8||| @ P the type of the proof
9−data Pair : (a : Type) -> (P : a -> Type) -> Type where
9+data Sigma : (a : Type) -> (P : a -> Type) -> Type where
10− pair : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Pair a P
10+ Sg_intro : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
11
11
12||| The eliminator for the empty type.
12||| The eliminator for the empty type.
13FalseElim : _|_ -> a
13FalseElim : _|_ -> a
libs/prelude/Prelude/Pairs.idr+5−5
@@ -31,12 +31,12 @@ using (a : Type, P : a -> Type)
31 getProof : (x : Subset a P) -> P (getWitness x)
31 getProof : (x : Subset a P) -> P (getWitness x)
32 getProof (element x pf) = pf
32 getProof (element x pf) = pf
33
33
34− namespace Pair
34+ namespace Sigma
35− getWitness : Pair a P -> a
35+ getWitness : Sigma a P -> a
36− getWitness (pair x pf) = x
36+ getWitness (x ** pf) = x
37
37
38− getProof : (x : Pair a P) -> P (getWitness x)
38+ getProof : (x : Sigma a P) -> P (getWitness x)
39− getProof (pair x pf) = pf
39+ getProof (x ** pf) = pf
40
40
41 -- Polymorphic (class-based) projections have been removed
41 -- Polymorphic (class-based) projections have been removed
42 -- because type-directed name disambiguation works better.
42 -- 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
1098 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1098 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1099
1099
1100-- Defined in builtins.idr
1100-- Defined in builtins.idr
1101−sigmaTy = sUN "Pair"
1101+sigmaTy = sUN "Sigma"
1102−existsCon = sUN "pair"
1102+existsCon = sUN "Sg_intro"
1103
1103
1104piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1104piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1105piBind = piBindp expl
1105piBind = piBindp expl
src/Idris/Delaborate.hs+2−2
@@ -92,13 +92,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
92 | n == eqCon = PRefl un (de env [] r)
92 | n == eqCon = PRefl un (de env [] r)
93 | n == sUN "lazy" = de env [] r
93 | n == sUN "lazy" = de env [] r
94 deFn env (P _ n _) [ty, Bind x (Lam _) r]
94 deFn env (P _ n _) [ty, Bind x (Lam _) r]
95− | n == sUN "Pair"
95+ | n == sUN "Sigma"
96 = PDPair un IsType (PRef un x) (de env [] ty)
96 = PDPair un IsType (PRef un x) (de env [] ty)
97 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
97 (de ((x,x):env) [] (instantiate (P Bound x ty) r))
98 deFn env (P _ n _) [_,_,l,r]
98 deFn env (P _ n _) [_,_,l,r]
99 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
99 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)
100 | n == eqTy = PEq un (de env [] l) (de env [] r)
100 | 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
102 (de env [] r)
102 (de env [] r)
103 deFn env f@(P _ n _) args
103 deFn env f@(P _ n _) args
104 | n `elem` map snd env
104 | n `elem` map snd env