core-spec: Modify `.lhs` to `.hs` (source files)

Modify old filename `.lhs` to `.hs` in following files:

  * docs/core-spec/README
  * docs/core-spec/CoreLint.ott
  * docs/core-spec/CoreSyn.ott
  * docs/core-spec/core-spec.mng

[ci skip]

4 files changed, 80 insertions, 80 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 6ace483cb5..606e45c190 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -12,7 +12,7 @@
 defns
 CoreLint :: '' ::=
 
-defn |- prog program ::  :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreBindings} }}
+defn |- prog program ::  :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{coreSyn/CoreLint.hs}{lintCoreBindings} }}
   {{ tex \labeledjudge{prog} [[program]] }}
 by
 
@@ -22,7 +22,7 @@ no_duplicates </ bindingi // i />
 --------------------- :: CoreBindings
 |-prog </ bindingi // i />
 
-defn G |- bind binding ::  :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{coreSyn/CoreLint.lhs}{lint\_bind} }}
+defn G |- bind binding ::  :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{coreSyn/CoreLint.hs}{lint\_bind} }}
   {{ tex [[G]] \labeledjudge{bind} [[binding]] }}
 by
 
@@ -34,7 +34,7 @@ G |-bind n = e
 ---------------------- :: Rec
 G |-bind rec </ ni = ei // i />
 
-defn G  |- sbind n <- e ::  :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
+defn G  |- sbind n <- e ::  :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding} }}
   {{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }}
 by
 
@@ -45,7 +45,7 @@ G |-name z_t ok
 ----------------- :: SingleBinding
 G |-sbind z_t <- e
 
-defn G ; D |-sjbind l vars <- e : t ::  :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
+defn G ; D |-sjbind l vars <- e : t ::  :: lintSingleBinding_joins :: 'SJBinding_' {{ com Single join binding typing, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding} }}
   {{ tex [[G]];[[D]] \labeledjudge{sjbind} [[l]] \, [[vars]] [[<-]] [[e]] : [[t]] }}
 by
 
@@ -60,7 +60,7 @@ split_I s = </ sj // j /> t
 G; D |-sjbind p/I_s </ nj // j /> <- e : t
 
 defn G ; D  |- tm e : t ::  :: lintCoreExpr :: 'Tm_'
-  {{ com Expression typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreExpr} }}
+  {{ com Expression typing, \coderef{coreSyn/CoreLint.hs}{lintCoreExpr} }}
   {{ tex [[G]]; [[D]] \labeledjudge{tm} [[e]] : [[t]] }}
 by
 
@@ -171,7 +171,7 @@ G |-co g : t1 k1~Rep k2 t2
 G; D |-tm g : (~Rep#) k1 k2 t1 t2
 
 defn G  |- name n ok ::  :: lintSingleBinding_lintBinder :: 'Name_'
-  {{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }}
+  {{ com Name consistency check, \coderef{coreSyn/CoreLint.hs}{lintSingleBinding\#lintBinder} }}
   {{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }}
 by
 
@@ -197,7 +197,7 @@ k' = * \/ k' = #
 G |-label p / I _ t ok
 
 defn G |- bnd n ok ::  :: lintBinder :: 'Binding_'
-  {{ com Binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintBinder} }}
+  {{ com Binding consistency, \coderef{coreSyn/CoreLint.hs}{lintBinder} }}
   {{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }}
 by
 
@@ -211,7 +211,7 @@ G |-ki k ok
 G |-bnd alpha_k ok
 
 defn G  |- co g : t1 k1 ~ R k2 t2 ::  :: lintCoercion :: 'Co_'
-  {{ com Coercion typing, \coderef{coreSyn/CoreLint.lhs}{lintCoercion} }}
+  {{ com Coercion typing, \coderef{coreSyn/CoreLint.hs}{lintCoercion} }}
   {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{ {}^{[[k1]]} {\sim}_{[[R]]}^{[[k2]]} } [[t2]] }}
 by
 
@@ -365,7 +365,7 @@ G |-ty t'2 : k0'
 G |-co mu </ ti // i /> $ </ gj // j /> : t'1 k0 ~R' k0' t'2
 
 defn G |- axk [ namesroles |-> gs ] ~> ( subst1 , subst2 ) ::  :: check_ki :: 'AxiomKind_'
-  {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.lhs}{lintCoercion\#check\_ki} }}
+  {{ com Axiom argument kinding, \coderef{coreSyn/CoreLint.hs}{lintCoercion\#check\_ki} }}
   {{ tex [[G]] \labeledjudge{axk} [ [[namesroles]] [[|->]] [[gs]] ] [[~>]] ([[subst1]], [[subst2]]) }}
 by
 
@@ -379,7 +379,7 @@ G |-co g0 : t1 {subst1(k)}~R subst2(k) t2
 G |-axk [ namesroles, n_R |-> gs, g0 ] ~> (subst1 [n |-> t1], subst2 [n |-> t2])
 
 defn validRoles T ::  :: checkValidRoles :: 'Cvr_'
-  {{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }}
+  {{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.hs}{checkValidRoles} }}
 by
 
 </ Ki // i /> = tyConDataCons T
@@ -389,7 +389,7 @@ by
 validRoles T
 
 defn validDcRoles </ Raa // aa /> K :: :: check_dc_roles :: 'Cdr_'
-  {{ com Data constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{check\_dc\_roles} }}
+  {{ com Data constructor role validity, \coderef{typecheck/TcTyClsDecls.hs}{check\_dc\_roles} }}
 by
 
 forall </ naa // aa />. forall </ mbb // bb />. </ tcc // cc /> $ -> T </ naa // aa /> = dataConRepType K
@@ -398,7 +398,7 @@ forall </ naa // aa />. forall </ mbb // bb />. </ tcc // cc /> $ -> T </ naa //
 validDcRoles </ Raa // aa /> K
 
 defn O |- t : R  ::   :: check_ty_roles :: 'Ctr_'
-  {{ com Type role validity, \coderef{typecheck/TcTyClsDecls.lhs}{check\_ty\_roles} }}
+  {{ com Type role validity, \coderef{typecheck/TcTyClsDecls.hs}{check\_ty\_roles} }}
   {{ tex [[O]] \labeledjudge{ctr} [[t]] : [[R]] }}
 by
 
@@ -441,7 +441,7 @@ O |- t |> g : R
 O |- g : Ph
 
 defn R1 <= R2 ::  :: ltRole :: 'Rlt_'
-  {{ com Sub-role relation, \coderef{types/Coercion.lhs}{ltRole} }}
+  {{ com Sub-role relation, \coderef{types/Coercion.hs}{ltRole} }}
   {{ tex [[R1]] \leq [[R2]] }}
 by
 
@@ -455,7 +455,7 @@ R <= Ph
 R <= R
 
 defn G |- ki k ok ::  :: lintKind :: 'K_'
-  {{ com Kind validity, \coderef{coreSyn/CoreLint.lhs}{lintKind} }}
+  {{ com Kind validity, \coderef{coreSyn/CoreLint.hs}{lintKind} }}
   {{ tex [[G]] \labeledjudge{k} [[k]] [[ok]] }}
 by
 
@@ -468,7 +468,7 @@ G |-ty k : #
 G |-ki k ok
 
 defn G |- ty t : k ::  :: lintType :: 'Ty_'
-  {{ com Kinding, \coderef{coreSyn/CoreLint.lhs}{lintType} }}
+  {{ com Kinding, \coderef{coreSyn/CoreLint.hs}{lintType} }}
   {{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }}
 by
 
@@ -518,7 +518,7 @@ G |-co g : t1 k1 ~Rep k2 t2
 G |-ty g : (~Rep#) k1 k2 t1 t2
 
 defn G |- subst n |-> t ok ::  :: lintTyKind :: 'Subst_'
-  {{ com Substitution consistency, \coderef{coreSyn/CoreLint.lhs}{lintTyKind} }}
+  {{ com Substitution consistency, \coderef{coreSyn/CoreLint.hs}{lintTyKind} }}
   {{ tex [[G]] \labeledjudge{subst} [[n]] [[|->]] [[t]] [[ok]] }}
 by
 
@@ -527,7 +527,7 @@ G |-ty t : k
 G |-subst z_k |-> t ok
 
 defn G ; D ; s |- altern alt : t ::  :: lintCoreAlt :: 'Alt_'
-  {{ com Case alternative consistency, \coderef{coreSyn/CoreLint.lhs}{lintCoreAlt} }}
+  {{ com Case alternative consistency, \coderef{coreSyn/CoreLint.hs}{lintCoreAlt} }}
   {{ tex [[G]];[[D]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
 by
 
@@ -552,7 +552,7 @@ G'; D |-tm e : t
 G; D; T </ sj // j /> |-altern K </ ni // i /> -> e : t
 
 defn t' = t { </ si // , // i /> } ::  :: applyTys :: 'ApplyTys_'
-  {{ com Telescope substitution, \coderef{types/Type.lhs}{applyTys} }}
+  {{ com Telescope substitution, \coderef{types/Type.hs}{applyTys} }}
 by
 
 --------------------- :: Empty
@@ -564,7 +564,7 @@ t'' = t'[n |-> s]
 t'' = (forall n. t) { s, </ si // i /> }
 
 defn G |- altbnd vars : t1 ~> t2 ::  :: lintAltBinders :: 'AltBinders_'
-  {{ com Case alternative binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintAltBinders} }}
+  {{ com Case alternative binding consistency, \coderef{coreSyn/CoreLint.hs}{lintAltBinders} }}
   {{ tex [[G]] \labeledjudge{altbnd} [[vars]] : [[t1]] [[~>]] [[t2]] }}
 by
 
@@ -585,7 +585,7 @@ G |-altbnd </ ni // i /> : t2 ~> s
 G |-altbnd x_t1, </ ni // i /> : (t1 -> t2) ~> s
 
 defn G |- arrow k1 -> k2 : k ::  :: lintArrow :: 'Arrow_'
-  {{ com Arrow kinding, \coderef{coreSyn/CoreLint.lhs}{lintArrow} }}
+  {{ com Arrow kinding, \coderef{coreSyn/CoreLint.hs}{lintArrow} }}
   {{ tex [[G]] \labeledjudge{\rightarrow} [[k1]] [[->]] [[k2]] : [[k]] }}
 by
 
@@ -595,7 +595,7 @@ k2 = TYPE s
 G |-arrow k1 -> k2 : *
 
 defn G |- app kinded_types : k1 ~> k2 ::  :: lint_app :: 'App_'
-  {{ com Type application kinding, \coderef{coreSyn/CoreLint.lhs}{lint\_app} }}
+  {{ com Type application kinding, \coderef{coreSyn/CoreLint.hs}{lint\_app} }}
   {{ tex [[G]] \labeledjudge{app} [[kinded_types]] : [[k1]] [[~>]] [[k2]] }}
 by
 
@@ -611,7 +611,7 @@ G |-app </ (ti : ki) // i /> : k2[z_k1 |-> t] ~> k'
 G |-app (t : k1), </ (ti : ki) // i /> : (forall z_k1. k2) ~> k'
 
 defn no_conflict ( C , </ sj // j /> , ind1 , ind2 ) ::  :: check_no_conflict :: 'NoConflict_'
-  {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.lhs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.lhs}{compatibleBranches} } }}
+  {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.hs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.hs}{compatibleBranches} } }}
 by
 
 ------------------------------------------------ :: NoBranch
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index b11730c276..cb9f1fc275 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -34,19 +34,19 @@ indexvar i, j, kk {{ tex k }}, aa {{ tex a }}, bb {{ tex b }}, cc {{ tex c }} ::
 grammar
 
 lit {{ tex \textsf{lit} }} :: 'Literal_' ::=
-  {{ com Literals, \coderef{basicTypes/Literal.lhs}{Literal} }}
+  {{ com Literals, \coderef{basicTypes/Literal.hs}{Literal} }}
 
 z :: 'Name_' ::= {{ com Term or type name }}
   | alpha           ::   :: Type    {{ com Type-level name }}
   | x               ::   :: Term    {{ com Term-level name }}
 
-n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.lhs}{Var} }}
+n, m, aname {{ tex \alpha }}, xname {{ tex x }} :: 'Var_' ::= {{ com Variable names, \coderef{basicTypes/Var.hs}{Var} }}
   | z _ t           ::   :: IdOrTyVar   {{ com Name, labeled with type/kind }}
     {{ tex {[[z]]}^{[[t]]} }}
   | z $             :: M :: NoSupScript {{ com Name without an explicit type/kind }}
   | K               :: M :: DataCon     {{ com Data constructor }}
 
-l :: 'Label_' ::= {{ com Labels for join points, also \coderef{basicTypes/Var.lhs}{Var} }}
+l :: 'Label_' ::= {{ com Labels for join points, also \coderef{basicTypes/Var.hs}{Var} }}
   | p / I _ t     ::   :: Label   {{ com Label with join arity and type }}
     {{ tex  {[[p]]}_{[[I]]}^{[[t]]} }}
 
@@ -64,7 +64,7 @@ labels :: 'Labels_' ::= {{ com List of labels }}
   | </ li // , // i />       ::   :: List
   | empty                    :: M :: empty
 
-e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
+e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.hs}{Expr} }}
   | n                                            ::   :: Var  {{ com \ctor{Var}: Variable }}
   | lit                                          ::   :: Lit  {{ com \ctor{Lit}: Literal }}
   | e1 e2                                        ::   :: App  {{ com \ctor{App}: Application }}
@@ -85,31 +85,31 @@ e, u :: 'Expr_' ::= {{ com Expressions, \coderef{coreSyn/CoreSyn.lhs}{Expr} }}
   | \\ e                                         :: M :: Newline
     {{ tex \qquad \\ \multicolumn{1}{r}{[[e]]} }}
 
-binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
+binding :: 'Bind_' ::= {{ com Let-bindings, \coderef{coreSyn/CoreSyn.hs}{Bind} }}
   | n = e                         ::   :: NonRec  {{ com \ctor{NonRec}: Non-recursive binding }}
   | rec </ ni = ei // ;; // i /> ::   :: Rec     {{ com \ctor{Rec}: Recursive binding }}
 
-jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{coreSyn/CoreSyn.lhs}{Bind} }}
+jbinding :: 'JoinBind_' ::= {{ com Join bindings, also \coderef{coreSyn/CoreSyn.hs}{Bind} }}
   | l </ ni // i /> = e     ::   :: NonRec {{ com \ctor{NonRec}: Non-recursive binding }}
   | rec </ li </ nij // j /> = ei // i /> :: :: Rec {{ com \ctor{Rec}: Recursive binding }}
 
-alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.lhs}{Alt} }}
+alt :: 'Alt_' ::= {{ com Case alternative, \coderef{coreSyn/CoreSyn.hs}{Alt} }}
   | Kp </ ni // i /> -> e    ::   :: Alt  {{ com Constructor applied to fresh names }}
 
-tick :: 'Tickish_' ::= {{ com Internal notes, \coderef{coreSyn/CoreSyn.lhs}{Tickish} }}
+tick :: 'Tickish_' ::= {{ com Internal notes, \coderef{coreSyn/CoreSyn.hs}{Tickish} }}
 
-Kp {{ tex \mathbb{K} }} :: 'AltCon_' ::= {{ com Constructors used in patterns, \coderef{coreSyn/CoreSyn.lhs}{AltCon} }}
+Kp {{ tex \mathbb{K} }} :: 'AltCon_' ::= {{ com Constructors used in patterns, \coderef{coreSyn/CoreSyn.hs}{AltCon} }}
   | K        ::   :: DataAlt         {{ com \ctor{DataAlt}: Data constructor }}
   | lit      ::   :: LitAlt          {{ com \ctor{LitAlt}: Literal (such as an integer or character) }}
   | _        ::   :: DEFAULT         {{ com \ctor{DEFAULT}: Wildcard }}
 
-program :: 'CoreProgram_' ::= {{ com A System FC program, \coderef{coreSyn/CoreSyn.lhs}{CoreProgram} }}
+program :: 'CoreProgram_' ::= {{ com A System FC program, \coderef{coreSyn/CoreSyn.hs}{CoreProgram} }}
   | </ bindingi // i />  ::   :: CoreProgram  {{ com List of bindings }}
 
 %% TYPES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
-  :: 'Type_' ::= {{ com Types/kinds, \coderef{types/TyCoRep.lhs}{Type} }}
+  :: 'Type_' ::= {{ com Types/kinds, \coderef{types/TyCoRep.hs}{Type} }}
   | n                       ::   :: TyVarTy       {{ com \ctor{TyVarTy}: Variable }}
   | t1 t2                   ::   :: AppTy         {{ com \ctor{AppTy}: Application }}
   | T </ ti // i />         ::   :: TyConApp      {{ com \ctor{TyConApp}: Application of type constructor }}
@@ -118,12 +118,12 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
   | lit                     ::   :: LitTy         {{ com \ctor{LitTy}: Type-level literal }}
   | t |> g                  ::   :: CastTy        {{ com \ctor{CastTy}: Kind cast }}
   | g                       ::   :: CoercionTy    {{ com \ctor{CoercionTy}: Coercion used in type }}
-  | tyConKind T             :: M :: tyConKind     {{ com \coderef{types/TyCon.lhs}{tyConKind} }}
+  | tyConKind T             :: M :: tyConKind     {{ com \coderef{types/TyCon.hs}{tyConKind} }}
   | t1 k1 ~# k2 t2          :: M :: unliftedEq    {{ com Metanotation for coercion types }}
     {{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\#}^{[[k2]]} } [[t2]] }}
   | t1 k1 ~Rep# k2 t2         :: M :: unliftedREq   {{ com Metanotation for coercion types }}
     {{ tex [[t1]] \mathop{ {}^{[[k1]]}\!\! \sim_{\mathsf{R}\#}^{[[k2]]} } [[t2]] }}
-  | literalType lit         :: M :: literalType   {{ com \coderef{basicTypes/Literal.lhs}{literalType} }}
+  | literalType lit         :: M :: literalType   {{ com \coderef{basicTypes/Literal.hs}{literalType} }}
   | ( t )                   :: M :: parens        {{ com Parentheses }}
   | { t }                   :: M :: IParens       {{ com Invisible parentheses }}
     {{ tex [[t]] }}
@@ -137,7 +137,7 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
 
 %% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.lhs}{Coercion} }}
+g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.hs}{Coercion} }}
   | < t >                   ::   :: Refl          {{ com \ctor{Refl}: Nominal Reflexivity }}
     {{ tex {\langle [[t]] \rangle} }}
   | < t > R mg              ::   :: GRefl         {{ com \ctor{GRefl}: Generalized Reflexivity }}
@@ -163,7 +163,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
   | ( g )                   :: M :: Parens        {{ com Parentheses }}
   | t $ liftingsubst        :: M :: Lifted        {{ com Type lifted to coercion }}
 
-prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.lhs}{UnivCoProvenance} }}
+prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.hs}{UnivCoProvenance} }}
   | UnsafeCoerceProv   ::   :: UnsafeCoerceProv  {{ com From \texttt{unsafeCoerce\#} }}
     {{ tex \mathsf{unsafe} }}
   | PhantomProv        ::   :: PhantomProv       {{ com From the need for a phantom coercion }}
@@ -171,20 +171,20 @@ prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/
   | ProofIrrelProv     ::   :: ProofIrrelProv    {{ com From proof irrelevance }}
     {{ tex \mathsf{irrel} }}
 
-mg {{ tex m }} :: 'MCoercion_' ::= {{ com A possibly reflexive coercion , \coderef{types/TyCoRep.lhs}{MCoercion} }}
+mg {{ tex m }} :: 'MCoercion_' ::= {{ com A possibly reflexive coercion , \coderef{types/TyCoRep.hs}{MCoercion} }}
   | MRefl            ::   :: MRefl                {{ com \ctor{MRefl}: A trivial reflexive coercion }}
   | MCo g            ::   :: MCo                  {{ com \ctor{MCo}: Other coercions }}
     {{ tex [[g]] }}
 
-LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.lhs}{LeftOrRight} }}
+LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.hs}{LeftOrRight} }}
   | Left             ::   :: CLeft                {{ com \ctor{CLeft}: Left projection }}
   | Right            ::   :: CRight               {{ com \ctor{CRight}: Right projection }}
 
-C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.lhs}{CoAxiom} }}
+C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.hs}{CoAxiom} }}
   | T RA </ axBranchi // ; // i />     ::   :: CoAxiom  {{ com \ctor{CoAxiom}: Axiom }}
   | ( C )                              :: M :: Parens   {{ com Parentheses }}
 
-R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.lhs}{Role} }}
+R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.hs}{Role} }}
   | Nom              ::   :: Nominal              {{ com Nominal }}
     {{ tex \mathsf{N} }}
   | Rep              ::   :: Representational     {{ com Representational }}
@@ -193,17 +193,17 @@ R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{types/CoAxiom.lhs}{Role}
     {{ tex \mathsf{P} }}
   | role_list [ i ]  :: M :: RoleListIndex        {{ com Look up in list }}
 
-axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.lhs}{CoAxBranch} }}
+axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.hs}{CoAxBranch} }}
   | forall </ ni RAi // i /> . ( </ tj // j /> ~> s )  ::   :: CoAxBranch  {{ com \ctor{CoAxBranch}: Axiom branch }}
   | ( </ axBranchi // i /> ) [ ind ]               :: M :: lookup      {{ com List lookup }}
 
-mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxiom.lhs}{CoAxiomRule} }}
+mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{types/CoAxiom.hs}{CoAxiomRule} }}
   | M ( I , role_list , R' )   ::  :: CoAxiomRule  {{ com Named rule, with parameter info }}
     {{ tex {[[M]]}_{([[I]], [[ role_list ]], [[R']])} }}
 
 %% TYCONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
+T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.hs}{TyCon} }}
   | ( -> )       ::   :: FunTyCon          {{ com \ctor{FunTyCon}: Arrow }}
 
   % the following also includes TupleTyCon, SynTyCon
@@ -213,7 +213,7 @@ T :: 'TyCon_' ::= {{ com Type constructors, \coderef{types/TyCon.lhs}{TyCon} }}
   | ' K          ::   :: PromotedDataCon   {{ com \ctor{PromotedDataCon}: Promoted data constructor }}
   | dataConTyCon K :: M :: dataConTyCon    {{ com TyCon extracted from DataCon }}
 
-H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{prelude/TysPrim.lhs}{} }}
+H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{prelude/TysPrim.hs}{} }}
   | Int#         ::   :: intPrimTyCon           {{ com Unboxed Int (\texttt{intPrimTyCon}) }}
   | ( ~# )       ::   :: eqPrimTyCon            {{ com Unboxed equality (\texttt{eqPrimTyCon}) }}
   | ( ~Rep# )      ::   :: eqReprPrimTyCon        {{ com Unboxed representational equality (\texttt{eqReprPrimTyCon}) }}
@@ -224,22 +224,22 @@ H :: 'PrimTyCon_' ::= {{ com Primitive type constructors, \coderef{prelude/TysPr
   | TYPE         ::   :: TYPE                   {{ com TYPE (\texttt{tYPETyCon}) }}
   | Levity       ::   :: Levity                 {{ com Levity (\texttt{LevityTyCon}) }}
 
-K :: 'DataCon_' ::= {{ com Data constructors, \coderef{basicTypes/DataCon.lhs}{DataCon} }}
+K :: 'DataCon_' ::= {{ com Data constructors, \coderef{basicTypes/DataCon.hs}{DataCon} }}
   | Lifted       ::   :: Lifted       {{ com \ctor{Lifted}, a lifted type }}
   | Unlifted     ::   :: Unlifted     {{ com \ctor{Unlifted}, an unlifted type }}
 
 %% CONTEXTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
+G {{ tex \Gamma }} :: 'LintM_Bindings_' ::= {{ com List of bindings, \coderef{coreSyn/CoreLint.hs}{LintM} }}
   | n                        ::   :: Binding   {{ com Single binding }}
   | </ Gi // , // i />       ::   :: Concat    {{ com Context concatenation }}
-  | vars_of binding          :: M :: VarsOf    {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
+  | vars_of binding          :: M :: VarsOf    {{ com \coderef{coreSyn/CoreSyn.hs}{bindersOf} }}
 
-D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.lhs}{LintM} }}
+D {{ tex \Delta }} :: 'LintM_JoinBindings_' ::= {{ com List of join bindings, \coderef{coreSyn/CoreLint.hs}{LintM} }}
   | l                        ::   :: Binding   {{ com Single binding }}
   | </ Di // , // i />       ::   :: Concat    {{ com Context concatenation }}
   | empty                    :: M :: Empty     {{ com Empty context }}
-  | labels_of binding        :: M :: LabelsOf  {{ com \coderef{coreSyn/CoreSyn.lhs}{bindersOf} }}
+  | labels_of binding        :: M :: LabelsOf  {{ com \coderef{coreSyn/CoreSyn.hs}{bindersOf} }}
 
 O {{ tex \Omega }} :: 'VarEnv_Role_' ::= {{ com Mapping from type variables to roles }}
   | </ ni : Ri // i />       ::   :: List      {{ com List of bindings }}
diff --git a/docs/core-spec/README b/docs/core-spec/README
index 1fb304d261..db864338c6 100644
--- a/docs/core-spec/README
+++ b/docs/core-spec/README
@@ -30,7 +30,7 @@ into LaTeX math-mode code. Thus, the file core-spec.mng is the source for
 core-spec.tex, which gets processed into core-spec.pdf.
 
 The file CoreSyn.ott contains the grammar of System FC, mostly extracted from
-compiler/coreSyn/CoreSyn.lhs. Here are a few pointers to help those of you
+compiler/coreSyn/CoreSyn.hs. Here are a few pointers to help those of you
 unfamiliar with Ott:
 
 - The {{ ... }} snippets are called "homs", and they assist ott in translating
@@ -69,7 +69,7 @@ your notation to LaTeX. Three different homs are used:
   it if necessary to disambiguate other parses.
 
 The file CoreLint.ott contains inductively defined judgements for many of the
-functions in compiler/coreSyn/CoreLint.lhs. Each judgement is labeled with an
+functions in compiler/coreSyn/CoreLint.hs. Each judgement is labeled with an
 abbreviation to distinguish it from the others. These abbreviations appear in
 the source code right after a turnstile |-. The declaration for each judgment
 contains a reference to the function it represents. Each rule is labeled with
@@ -80,4 +80,4 @@ If you need help with these files or do not know how to edit them, please
 contact Richard Eisenberg (eir@cis.upenn.edu).
 
 [1] http://www.cl.cam.ac.uk/~pes20/ott/
-[2] http://www.cl.cam.ac.uk/~pes20/ott/ott_manual_0.21.2.pdf
\ No newline at end of file
+[2] http://www.cl.cam.ac.uk/~pes20/ott/ott_manual_0.21.2.pdf
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index bdebc32c90..3064a556e3 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -71,8 +71,8 @@ Literals do not play a major role, so we leave them abstract:
 
 \gram{\ottlit}
 
-We also leave abstract the function \coderef{basicTypes/Literal.lhs}{literalType}
-and the judgment \coderef{coreSyn/CoreLint.lhs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
+We also leave abstract the function \coderef{basicTypes/Literal.hs}{literalType}
+and the judgment \coderef{coreSyn/CoreLint.hs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
 
 \subsection{Variables}
 \enlargethispage{10pt} % without this first line of "z" definition is placed on
@@ -109,7 +109,7 @@ $[[let]]$ may be of type \texttt{Addr\#} if it's a primitive string literal.
 See \verb|#top_level_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
 \item The right-hand side of a non-recursive $[[let]]$ and the argument
 of an application may be of unlifted type, but only if the expression
-is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.lhs}.
+is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
 \item We allow a non-recursive $[[let]]$ for bind a type variable.
 \item The $[[_]]$ case for a $[[case]]$ must come first.
 \item The list of case alternatives must be exhaustive.
@@ -119,7 +119,7 @@ In other words, the payload inside of a \texttt{Type} constructor must not turn
 to be built with \texttt{CoercionTy}.
 \item Join points (introduced by $[[join]]$ expressions) follow the invariants
 laid out in \verb|Note [Invariants on join points]| in
-\ghcfile{coreSyn/CoreSyn.lhs}:
+\ghcfile{coreSyn/CoreSyn.hs}:
 \begin{enumerate}
     \item All occurences must be tail calls. This is enforced in our typing
     rules using the label environment $[[D]]$.
@@ -170,9 +170,9 @@ A program is just a list of bindings:
 \gram{\ottt}
 
 \ctor{FunTy} is the special case for non-dependent function type. The
-\ctor{TyBinder} in \ghcfile{types/TyCoRep.lhs} distinguishes whether a binder is
+\ctor{TyBinder} in \ghcfile{types/TyCoRep.hs} distinguishes whether a binder is
 anonymous (\ctor{FunTy}) or named (\ctor{ForAllTy}). See
-\verb|Note [TyBinders]| in \ghcfile{types/TyCoRep.lhs}.
+\verb|Note [TyBinders]| in \ghcfile{types/TyCoRep.hs}.
 
 There are some invariants on types:
 \begin{itemize}
@@ -284,8 +284,8 @@ type arity $[[I]]$, a list of roles $[[role_list]]$ for its coercion parameters,
 and an output role $[[R']]$. The definition within GHC also includes a field named
 $[[coaxrProves]]$ which computes the output coercion from a list of types and
 a list of coercions. This is elided in this presentation, as we simply identify
-axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
-and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
+axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.hs}{mkBinAxiom}
+and \coderef{typecheck/TcTypeNats.hs}{mkAxiom1}.
 
 In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands for following checks:
 \begin{itemize}
@@ -296,7 +296,7 @@ In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands
     \item unboxed tuples should have same length and each element should be coercible to
     appropriate element of the target tuple;
 \end{itemize}
-For function implementation see \coderef{coreSyn/CoreLint.lhs}{checkTypes}.
+For function implementation see \coderef{coreSyn/CoreLint.hs}{checkTypes}.
 For further discussion see \url{https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions}.
 
 \subsection{Type constructors}
@@ -306,7 +306,7 @@ for this formalism:
 
 \gram{\ottT}
 
-We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.lhs}.
+We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.hs}.
 
 \gram{\ottH}
 
@@ -327,7 +327,7 @@ synonym for $[[TYPE 'Unlifted]]$.
 
 \section{Contexts}
 
-The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
+The functions in \ghcfile{coreSyn/CoreLint.hs} use the \texttt{LintM} monad.
 This monad contains a context with a set of bound variables $[[G]]$ and a set
 of bound labels $[[D]]$. The formalism treats $[[G]]$ and $[[D]]$ as ordered
 lists, but GHC uses sets as its
@@ -347,13 +347,13 @@ fresh in the context. In the implementation, of course, some work is done
 to guarantee this freshness. In particular, adding a new type variable to
 the context sometimes requires creating a new, fresh variable name and then
 applying a substitution. We elide these details in this formalism, but
-see \coderef{types/Type.lhs}{substTyVarBndr} for details.
+see \coderef{types/Type.hs}{substTyVarBndr} for details.
 
 \section{Typing judgments}
 
 The following functions are used from GHC. Their names are descriptive, and they
-are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
-\coderef{types/TyCon.lhs}{tyConArity}, \coderef{basicTypes/DataCon.lhs}{dataConTyCon}, \coderef{types/TyCon.lhs}{isNewTyCon}, \coderef{basicTypes/DataCon.lhs}{dataConRepType}.
+are not formalized here: \coderef{types/TyCon.hs}{tyConKind},
+\coderef{types/TyCon.hs}{tyConArity}, \coderef{basicTypes/DataCon.hs}{dataConTyCon}, \coderef{types/TyCon.hs}{isNewTyCon}, \coderef{basicTypes/DataCon.hs}{dataConRepType}.
 
 \subsection{Program consistency}
 
@@ -363,7 +363,7 @@ and then check each binding.
 
 \ottdefnlintCoreBindings{}
 
-Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs}{bindersOf}:
+Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.hs}{bindersOf}:
 
 \[
 \begin{array}{ll}
@@ -409,11 +409,11 @@ to check each substituted type $[[s'i]]$ in a context containing all the types
 that come before it in the list of bindings. The $[[G'i]]$ are contexts
 containing the names and kinds of all type variables (and term variables,
 for that matter) up to the $i$th binding. This logic is extracted from
-\coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
+\coderef{coreSyn/CoreLint.hs}{lintAndScopeIds}.
 
 \item The GHC source code checks all arguments in an application expression
-all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
-and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
+all at once using \coderef{coreSyn/CoreSyn.hs}{collectArgs}
+and \coderef{coreSyn/CoreLint.hs}{lintCoreArgs}. The operation
 has been unfolded for presentation here.
 
 \item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
@@ -505,7 +505,7 @@ $[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to accou
 for potential oversaturation.
 
 The checks encoded in the following
-judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
+judgments are run from \coderef{typecheck/TcTyClsDecls.hs}{checkValidTyCon}
 when \texttt{-dcore-lint} is set.
 
 \ottdefncheckValidRoles{}
@@ -539,12 +539,12 @@ The judgment $[[apart]]$ checks to see whether two lists of types are surely
 apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i />
 ]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
 \emph{patterns} (as in a type family equation), first flattens the $[[ </ ti
-    // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to
-see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
+    // i /> ]]$ using \coderef{types/FamInstEnv.hs}{flattenTys} and then checks to
+see if \coderef{types/Unify.hs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
 Flattening takes all type family applications and replaces them with fresh variables,
 taking care to map identical type family applications to the same fresh variable.
 
-The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
+The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.hs}{tcUnifyTys}.
 It performs a standard unification, returning a substitution upon success.
 
 \section{Operational semantics}
@@ -553,7 +553,7 @@ It performs a standard unification, returning a substitution upon success.
 GHC does not implement an operational semantics in any concrete form. Most
 of the rules below are implied by algorithms in, for example, the simplifier
 and optimizer. Yet, there is no one place in GHC that states these rules,
-analogously to \texttt{CoreLint.lhs}.
+analogously to \texttt{CoreLint.hs}.
 Nevertheless, these rules are included in this document to help the reader
 understand System FC.
 
@@ -581,17 +581,17 @@ to the constructor. The terms are the regular term arguments stored in an
 algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
 \item The rule \ottdrulename{S\_CasePush} is the most complex rule.
 \begin{itemize}
-\item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
-\item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
+\item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.hs}{exprIsConApp\_maybe}.
+\item The $[[coercionKind]]$ function (\coderef{types/Coercion.hs}{coercionKind})
 extracts the two types (and their kinds) from
 a coercion. It does not require a typing context, as it does not \emph{check} the
 coercion, just extracts its types.
-\item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
+\item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.hs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
 constructor expressions, the parameters to the constructor are broken into three
 groups: universally quantified types, existentially quantified types, and terms.
 \item The substitutions in the last premise to the rule are unusual: they replace
 \emph{type} variables with \emph{coercions}. This substitution is called lifting
-and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
+and is implemented in \coderef{types/Coercion.hs}{liftCoSubst}. The notation is
 essentially a pun on the fact that types and coercions have such similar structure.
 This operation is quite non-trivial. Please see \emph{System FC with Explicit
 Kind Equality} for details.