Hoogle Search

Within LTS Haskell 24.38 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

Exact lookup

1. ForeignPragma :: Range -> Ranged BackendName -> String -> Pragma

   Agda	Agda.Syntax.Concrete

   No documentation available.

2. module Agda.TypeChecking.Forcing

   A constructor argument is forced if it appears as pattern variable in an index of the target. For instance x is forced in sing and n is forced in zero and suc:

   data Sing {a}{A : Set a} : A -> Set where
   sing : (x : A) -> Sing x
   
   data Fin : Nat -> Set where
   zero : (n : Nat) -> Fin (suc n)
   suc  : (n : Nat) (i : Fin n) -> Fin (suc n)
   

   At runtime, forced constructor arguments may be erased as they can be recovered from dot patterns. For instance, unsing : {A : Set} (x : A) -> Sing x -> A unsing .x (sing x) = x can become unsing x sing = x and proj : (n : Nat) (i : Fin n) -> Nat proj .(suc n) (zero n) = n proj .(suc n) (suc n i) = n becomes proj (suc n) zero = n proj (suc n) (suc i) = n This module implements the analysis of which constructor arguments are forced. The process of moving the binding site of forced arguments is implemented in the unifier (see the Solution step of Agda.TypeChecking.Rules.LHS.Unify.unifyStep). Forcing is a concept from pattern matching and thus builds on the concept of equality (I) used there (closed terms, extensional) which is different from the equality (II) used in conversion checking and the constraint solver (open terms, intensional). Up to issue 1441 (Feb 2015), the forcing analysis here relied on the wrong equality (II), considering type constructors as injective. This is unsound for program extraction, but ok if forcing is only used to decide which arguments to skip during conversion checking. From now on, forcing uses equality (I) and does not search for forced variables under type constructors. This may lose some savings during conversion checking. If this turns out to be a problem, the old forcing could be brought back, using a new modality Skip to indicate that this is a relevant argument but still can be skipped during conversion checking as it is forced by equality (II).

3. class (PrecomputeFreeVars a, Subst a) => ForceNotFree a

   Agda	Agda.TypeChecking.Free.Reduce

   No documentation available.

4. Forced :: IsForced

   Agda	Agda.TypeChecking.Monad.Base

   No documentation available.

5. ForcedConstructorNotInstantiated :: Pattern -> TypeError

   Agda	Agda.TypeChecking.Monad.Base

   No documentation available.

6. data ForeignCode

   Agda	Agda.TypeChecking.Monad.Base

   No documentation available.

7. ForeignCode :: Range -> String -> ForeignCode

   Agda	Agda.TypeChecking.Monad.Base

   No documentation available.

8. newtype ForeignCodeStack

   Agda	Agda.TypeChecking.Monad.Base

   Foreign code fragments are stored in reversed order to support efficient appending: head points to the latest pragma in module.

9. ForeignCodeStack :: [ForeignCode] -> ForeignCodeStack

   Agda	Agda.TypeChecking.Monad.Base

   No documentation available.

10. FormulaToFloating :: DealStats -> Floater -> RateSwapType

    Hastructure	Hedge

    Paying Formula Rate and receiving Floating rate

Page 321 of many | Previous | Next