Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

export fixity declarations #71

Merged
merged 1 commit into from
Mar 31, 2024
Merged

export fixity declarations #71

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Data/Relation.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ public export
0 Rel : Type -> Type
Rel a = a -> a -> Type

infix 5 ~>
export infix 5 ~>
public export
0 (~>) : Rel a -> Rel a -> Type
p ~> q = {x, y : a} -> p x y -> q x y
2 changes: 1 addition & 1 deletion src/Data/Setoid/Definition.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import public Control.Order
import Data.Vect
import public Data.Fun.Nary

infix 5 ~>, ~~>, <~>
export infix 5 ~>, ~~>, <~>

%default total

Expand Down
4 changes: 2 additions & 2 deletions src/Frex/Algebra.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,8 @@ import Data.Stream
import Data.Name
import Data.Vect.Extra

infix 10 ^
infix 5 ~>, <~>
export infix 10 ^
export infix 5 ~>, <~>

%default total

Expand Down
2 changes: 1 addition & 1 deletion src/Frex/Axiom.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import Data.Fin

%default total

infix 1 =-=
export infix 1 =-=

||| Smart constructor for making equations look nicer
public export
Expand Down
2 changes: 1 addition & 1 deletion src/Frex/Coproduct.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import Frex.Presentation
import Frex.Algebra
import Frex.Model

infixr 3 <~.~>
export infixr 3 <~.~>

%default total

Expand Down
2 changes: 1 addition & 1 deletion src/Frex/Free/Construction.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ import Text.PrettyPrint.Prettyprinter

%default total

infix 4 |-
export infix 4 |-

||| Auxiliary abstraction: an algebra with a relation over it
public export
Expand Down
2 changes: 1 addition & 1 deletion src/Frex/Free/Construction/Linear.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ plug : (a : Algebra sig) ->
(t : U a) -> U a
plug a t u = bindTerm t (fromMaybe u)

infixr 0 :.:
export infixr 0 :.:
public export
(:.:) : {0 sig : Signature} ->
Term sig (Maybe a) ->
Expand Down
2 changes: 1 addition & 1 deletion src/Frex/Model.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ import Data.Vect.Extra
import Data.Vect.Quantifiers
import Data.Fin

infix 1 =|
export infix 1 =|

%default total
%ambiguity_depth 4
Expand Down
2 changes: 1 addition & 1 deletion src/Notation/Additive.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import public Data.Fun.Extra

%default total

infixl 8 .+., :+:, |+|, +., +:, +|, .+, :+, |+
export infixl 8 .+., :+:, |+|, +., +:, +|, .+, :+, |+

public export
interface Additive1 a where
Expand Down
2 changes: 1 addition & 1 deletion src/Notation/Multiplicative.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import public Data.Fun.Extra

%default total

infixl 9 .*., :*:, |*|, *., *:, *|, .*, :*, |*
export infixl 9 .*., :*:, |*|, *., *:, *|, .*, :*, |*

public export
interface Multiplicative1 a where
Expand Down
6 changes: 3 additions & 3 deletions src/Syntax/PreorderReasoning/Setoid.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ module Syntax.PreorderReasoning.Setoid

import Data.Setoid.Definition

infixl 0 ~~
prefix 1 |~
infix 1 ...,..<,..>,.=.,.=<,.=>
export infixl 0 ~~
export prefix 1 |~
export infix 1 ...,..<,..>,.=.,.=<,.=>

public export
data Step : (a : Setoid) -> (lhs,rhs : U a) -> Type where
Expand Down
2 changes: 1 addition & 1 deletion tests/frextests/certificates/Monoids.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ import Syntax.PreorderReasoning

import System.File

infix 0 ~~
export infix 0 ~~
0 (~~) : Rel (U (Construction.Free MonoidTheory $ cast $ Fin n).Data.Model)
(~~) = (Free MonoidTheory $ cast $ Fin n).Data.Model.rel

Expand Down
2 changes: 1 addition & 1 deletion tests/frextests/printer/CommutativeMonoids.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ Sta' = (FrexNat).Data.Embed.H.H
Dyn' : {0 x : Type} -> x -> U (FrexNat {x}).Data.Model
Dyn' = (FrexNat {x}).Data.Var.H

infix 0 ~~
export infix 0 ~~
0 (~~) : (lhs, rhs : Term (EvaluationSig (CommutativeMonoidTheory).signature Nat) x) -> Type
(~~) = (FrexNat).Data.Model.rel

Expand Down
2 changes: 1 addition & 1 deletion tests/frextests/printer/Monoids.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ import System.File
show _ = "boring"

-- Using a concrete name so that the constraints when forming `X k` compute
infix 0 ~~
export infix 0 ~~
(~~) : Term Signature (Fin 10) -> Term Signature (Fin 10) -> Type
(~~) = (|-) {pres = MonoidTheory}
(QuotientData MonoidTheory (irrelevantCast (Fin 10)))
Expand Down
Loading