idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Typos: change all uses of inferable to inferrable

Browse Source 
Achieves consistency...
This commit is contained in:
Walter Smuts 2023-06-08 13:35:52 +02:00
parent e86420f710
commit 98e5615dbc
2 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libs/papers/Language/IntrinsicScoping/TypeTheory.idr
View File

@ -63,9 +63,9 @@ data Infer : Scoped where
-- This is fairly unconventional: in order to support overloaded
-- data constructors disambiguated in a type-direct manner, we would
-- typically put zero, suc, & friends in `Check`.
||| The zero constructor is inferable
||| The zero constructor is inferrable
Zro : Infer f g
||| The successor constructor is inferable
||| The successor constructor is inferrable
Suc : Check f g -> Infer f g
||| Pi is inferrable
Pi : (a : Check f g) -> (b : Abs Check f g) -> Infer f g
@ -82,7 +82,7 @@ infixl 3 `App`
total
data Check : Scoped where
||| Inferable terms are trivially checkable
||| Inferrable terms are trivially checkable
Emb : Infer f g -> Check f g
||| A function binding its argument
Lam : Abs Check f g -> Check f g

12
libs/papers/Language/TypeTheory.idr
View File

@ -74,7 +74,7 @@ namespace Section2
-- Raw terms are neither scopechecked nor typecked
||| Inferable terms know what their type is
||| Inferrable terms know what their type is
data Infer : Type
||| Checkable terms need to be checked against a type
@ -97,7 +97,7 @@ namespace Section2
total
data Check : Type where
||| Inferable terms are trivially checkable
||| Inferrable terms are trivially checkable
Emb : Infer -> Check
||| A function binding its argument
Lam : Abs Check -> Check
@ -365,7 +365,7 @@ namespace Section3
total
data Check : Type where
||| Inferable terms are trivially checkable
||| Inferrable terms are trivially checkable
Emb : Infer -> Check
||| A function binding its argument
Lam : Abs Check -> Check
@ -587,9 +587,9 @@ namespace Section4
-- ps : Abs (Abs Check)
-- n : Check
Rec : (pred, pz, ps : Check) -> (n : Check) -> Infer
||| The zero constructor is inferable
||| The zero constructor is inferrable
Zro : Infer
||| The successor constructor is inferable
||| The successor constructor is inferrable
Suc : Check -> Infer
||| Pi is inferrable
Pi : (a : Check) -> (b : Abs Check) -> Infer
@ -606,7 +606,7 @@ namespace Section4
total
data Check : Type where
||| Inferable terms are trivially checkable
||| Inferrable terms are trivially checkable
Emb : Infer -> Check
||| A function binding its argument
Lam : Abs Check -> Check