Skip to content

Commit 17f96c2

Browse files
jasagredojasagredo
authored
Do not align closing brackets in LANGUAGE (#1252)
The Agda files were just converted from CRLF to LF via dos2unix.
2 parents f042d6b + be83fd7 commit 17f96c2

File tree

470 files changed

+3598
-3598
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

470 files changed

+3598
-3598
lines changed

‎.stylish-haskell.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -424,7 +424,7 @@ steps:
424424
# between actual import and closing bracket.
425425
#
426426
# Default: true
427-
align: true
427+
align: false
428428

429429
# stylish-haskell can detect redundancy of some language pragmas. If this
430430
# is set to true, it will remove those redundant pragmas. Default: true.

‎docs/agda-spec/src/Data/Rational/Ext.agda‎

Lines changed: 66 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -1,66 +1,66 @@
1-
{-# OPTIONS --safe #-}
2-
3-
open import Agda.Primitive renaming (Set to Type)
4-
5-
module Data.Rational.Ext where
6-
7-
open import Function using (_∘_; _$_)
8-
open import Data.Rational
9-
open import Data.Rational.Properties
10-
open import Data.Product using (_×_; ∃-syntax)
11-
open import Data.Nat as ℕ using (ℕ)
12-
open import Data.Integer as ℤ using (ℤ; +_)
13-
open import Data.Integer.GCD using (gcd)
14-
import Data.Integer.Properties as ℤ
15-
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl)
16-
open import Relation.Binary.PropositionalEquality using (cong; sym; module ≡-Reasoning)
17-
open import Relation.Nullary.Negation using (contradiction)
18-
19-
-- The interval (0, 1]
20-
PosUnitInterval : Type
21-
PosUnitInterval = ∃[ p ] Positive p × p ≤ 1ℚ
22-
23-
record RationalExtStructure : Type where
24-
field
25-
exp : ℚ → ℚ
26-
ln : (p : ℚ) → ⦃ Positive p ⦄ → ℚ
27-
28-
p≢1⇒1-p≢0 : ∀ {p : ℚ} → p ≢ 1ℚ → 1ℚ - p ≢ 0ℚ
29-
p≢1⇒1-p≢0 {p} p≢1 1-p≡0 = contradiction p≡1 p≢1
30-
where
31-
open ≡-Reasoning
32-
p≡1 = sym $ begin
33-
1ℚ ≡⟨ sym $ +-identityʳ 1ℚ ⟩
34-
1ℚ + 0ℚ ≡⟨ cong (λ i → 1ℚ + i) (sym $ +-inverseˡ p) ⟩
35-
1ℚ + (- p + p) ≡⟨ sym $ +-assoc 1ℚ (- p) p ⟩
36-
(1ℚ - p) + p ≡⟨ cong (_+ p) 1-p≡0 ⟩
37-
0ℚ + p ≡⟨ +-identityˡ p ⟩
38-
p ∎
39-
40-
p≤1⇒1-p≥0 : ∀ {p : ℚ} → p ≤ 1ℚ → 1ℚ - p ≥ 0ℚ
41-
p≤1⇒1-p≥0 {p} p≤1 = +-monoʳ-≤ 1ℚ -p≥-1
42-
where
43-
-p≥-1 = neg-antimono-≤ p≤1
44-
45-
drop-≢ : ∀ {p q : ℚ} → p ≢ q → ↥ p ℤ.* ↧ q ≢ ↥ q ℤ.* ↧ p
46-
drop-≢ p≢q = p≢q ∘ ≃⇒≡ ∘ *≡*
47-
48-
≤∧≢⇒< : ∀ {p q : ℚ} → p ≤ q → p ≢ q → p < q
49-
≤∧≢⇒< p≤q p≢q = *<* $ ℤ.≤∧≢⇒< (drop-*≤* p≤q) (drop-≢ p≢q)
50-
51-
p≡1⇒↥p≡↧p : ∀ {p : ℚ} → p ≡ 1ℚ → ↥ p ≡ ↧ p
52-
p≡1⇒↥p≡↧p {p} p≡1
53-
rewrite sym (ℤ.*-identityʳ (↥ p))
54-
| drop-*≡* (≡⇒≃ p≡1)
55-
| ℤ.*-identityˡ (↧ p)
56-
= refl
57-
58-
↥p<↧p⇒p≢1 : ∀ {p : ℚ} → ↥ p ℤ.< ↧ p → p ≢ 1ℚ
59-
↥p<↧p⇒p≢1 n<m n/m≡1 = (ℤ.<⇒≢ n<m) (p≡1⇒↥p≡↧p n/m≡1)
60-
61-
n<m⇒↥[n/m]<↧[n/m] : ∀ {n m : ℕ} → ⦃ _ : ℕ.NonZero m ⦄ → n ℕ.< m → ↥ (+ n / m) ℤ.< ↧ (+ n / m)
62-
n<m⇒↥[n/m]<↧[n/m] {n} {m} n<m = ℤ.*-cancelʳ-<-nonNeg g $ begin-strict
63-
(↥ (+ n / m)) ℤ.* g ≡⟨ ↥-/ (+ n) m ⟩
64-
+ n <⟨ ℤ.+<+ n<m ⟩
65-
+ m ≡⟨ sym (↧-/ (+ n) m) ⟩
66-
↧ (+ n / m) ℤ.* g ∎ where open ℤ.≤-Reasoning; g = gcd (+ n) (+ m)
1+
{-# OPTIONS --safe #-}
2+
3+
open import Agda.Primitive renaming (Set to Type)
4+
5+
module Data.Rational.Ext where
6+
7+
open import Function using (_∘_; _$_)
8+
open import Data.Rational
9+
open import Data.Rational.Properties
10+
open import Data.Product using (_×_; ∃-syntax)
11+
open import Data.Nat as ℕ using (ℕ)
12+
open import Data.Integer as ℤ using (ℤ; +_)
13+
open import Data.Integer.GCD using (gcd)
14+
import Data.Integer.Properties as ℤ
15+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl)
16+
open import Relation.Binary.PropositionalEquality using (cong; sym; module ≡-Reasoning)
17+
open import Relation.Nullary.Negation using (contradiction)
18+
19+
-- The interval (0, 1]
20+
PosUnitInterval : Type
21+
PosUnitInterval = ∃[ p ] Positive p × p ≤ 1ℚ
22+
23+
record RationalExtStructure : Type where
24+
field
25+
exp : ℚ → ℚ
26+
ln : (p : ℚ) → ⦃ Positive p ⦄ → ℚ
27+
28+
p≢1⇒1-p≢0 : ∀ {p : ℚ} → p ≢ 1ℚ → 1ℚ - p ≢ 0ℚ
29+
p≢1⇒1-p≢0 {p} p≢1 1-p≡0 = contradiction p≡1 p≢1
30+
where
31+
open ≡-Reasoning
32+
p≡1 = sym $ begin
33+
1ℚ ≡⟨ sym $ +-identityʳ 1ℚ ⟩
34+
1ℚ + 0ℚ ≡⟨ cong (λ i → 1ℚ + i) (sym $ +-inverseˡ p) ⟩
35+
1ℚ + (- p + p) ≡⟨ sym $ +-assoc 1ℚ (- p) p ⟩
36+
(1ℚ - p) + p ≡⟨ cong (_+ p) 1-p≡0 ⟩
37+
0ℚ + p ≡⟨ +-identityˡ p ⟩
38+
p ∎
39+
40+
p≤1⇒1-p≥0 : ∀ {p : ℚ} → p ≤ 1ℚ → 1ℚ - p ≥ 0ℚ
41+
p≤1⇒1-p≥0 {p} p≤1 = +-monoʳ-≤ 1ℚ -p≥-1
42+
where
43+
-p≥-1 = neg-antimono-≤ p≤1
44+
45+
drop-≢ : ∀ {p q : ℚ} → p ≢ q → ↥ p ℤ.* ↧ q ≢ ↥ q ℤ.* ↧ p
46+
drop-≢ p≢q = p≢q ∘ ≃⇒≡ ∘ *≡*
47+
48+
≤∧≢⇒< : ∀ {p q : ℚ} → p ≤ q → p ≢ q → p < q
49+
≤∧≢⇒< p≤q p≢q = *<* $ ℤ.≤∧≢⇒< (drop-*≤* p≤q) (drop-≢ p≢q)
50+
51+
p≡1⇒↥p≡↧p : ∀ {p : ℚ} → p ≡ 1ℚ → ↥ p ≡ ↧ p
52+
p≡1⇒↥p≡↧p {p} p≡1
53+
rewrite sym (ℤ.*-identityʳ (↥ p))
54+
| drop-*≡* (≡⇒≃ p≡1)
55+
| ℤ.*-identityˡ (↧ p)
56+
= refl
57+
58+
↥p<↧p⇒p≢1 : ∀ {p : ℚ} → ↥ p ℤ.< ↧ p → p ≢ 1ℚ
59+
↥p<↧p⇒p≢1 n<m n/m≡1 = (ℤ.<⇒≢ n<m) (p≡1⇒↥p≡↧p n/m≡1)
60+
61+
n<m⇒↥[n/m]<↧[n/m] : ∀ {n m : ℕ} → ⦃ _ : ℕ.NonZero m ⦄ → n ℕ.< m → ↥ (+ n / m) ℤ.< ↧ (+ n / m)
62+
n<m⇒↥[n/m]<↧[n/m] {n} {m} n<m = ℤ.*-cancelʳ-<-nonNeg g $ begin-strict
63+
(↥ (+ n / m)) ℤ.* g ≡⟨ ↥-/ (+ n) m ⟩
64+
+ n <⟨ ℤ.+<+ n<m ⟩
65+
+ m ≡⟨ sym (↧-/ (+ n) m) ⟩
66+
↧ (+ n / m) ℤ.* g ∎ where open ℤ.≤-Reasoning; g = gcd (+ n) (+ m)

‎docs/agda-spec/src/InterfaceLibrary/Ledger.lagda‎

Lines changed: 36 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,36 @@
1-
\begin{code}[hide]
2-
{-# OPTIONS --safe #-}
3-
4-
-- TODO: The following should be likely located in Common.
5-
open import Ledger.Prelude
6-
open import Ledger.Crypto
7-
open import Ledger.Script
8-
open import Ledger.Types.Epoch
9-
10-
module InterfaceLibrary.Ledger
11-
(crypto : Crypto)
12-
(es : _) (open EpochStructure es)
13-
(ss : ScriptStructure crypto es) (open ScriptStructure ss)
14-
where
15-
16-
open import Ledger.PParams crypto es ss using (PParams)
17-
open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr)
18-
19-
\end{code}
20-
21-
\begin{figure*}[h]
22-
\begin{code}[hide]
23-
record LedgerInterface : Type₁ where
24-
field
25-
\end{code}
26-
\begin{code}
27-
NewEpochState : Type
28-
getPParams : NewEpochState → PParams
29-
getEpoch : NewEpochState → Epoch
30-
getPoolDistr : NewEpochState → PoolDistr
31-
adoptGenesisDelegs : NewEpochState → Slot → NewEpochState
32-
_⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type
33-
\end{code}
34-
\caption{Ledger interface}
35-
\label{fig:interface:ledger}
36-
\end{figure*}
1+
\begin{code}[hide]
2+
{-# OPTIONS --safe #-}
3+
4+
-- TODO: The following should be likely located in Common.
5+
open import Ledger.Prelude
6+
open import Ledger.Crypto
7+
open import Ledger.Script
8+
open import Ledger.Types.Epoch
9+
10+
module InterfaceLibrary.Ledger
11+
(crypto : Crypto)
12+
(es : _) (open EpochStructure es)
13+
(ss : ScriptStructure crypto es) (open ScriptStructure ss)
14+
where
15+
16+
open import Ledger.PParams crypto es ss using (PParams)
17+
open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr)
18+
19+
\end{code}
20+
21+
\begin{figure*}[h]
22+
\begin{code}[hide]
23+
record LedgerInterface : Type₁ where
24+
field
25+
\end{code}
26+
\begin{code}
27+
NewEpochState : Type
28+
getPParams : NewEpochState → PParams
29+
getEpoch : NewEpochState → Epoch
30+
getPoolDistr : NewEpochState → PoolDistr
31+
adoptGenesisDelegs : NewEpochState → Slot → NewEpochState
32+
_⊢_⇀⦇_,NEWEPOCH⦈_ : ⊤ → NewEpochState → Epoch → NewEpochState → Type
33+
\end{code}
34+
\caption{Ledger interface}
35+
\label{fig:interface:ledger}
36+
\end{figure*}

0 commit comments

Comments
 (0)