michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(doc/lua): typo

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-04 15:06:44 -07:00
parent bab430af43
commit a522398194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/lua/lua.md
View file

@ -451,7 +451,7 @@ apply basic simplifications automatically. However, they do not put
the level expressions in any normal form. We can use the method the level expressions in any normal form. We can use the method
`normalize` for that. The normalization procedure is also use to `normalize` for that. The normalization procedure is also use to
implement the method `is_equivalent` that returns true when two level implement the method `is_equivalent` that returns true when two level
expressions are equivalent. The Lua API also contains the methdo expressions are equivalent. The Lua API also contains the method
`is_geq` that can be used to check whether a level expression `is_geq` that can be used to check whether a level expression
represents a universe bigger than or equal another one. represents a universe bigger than or equal another one.