Viktor Yudov
Viktor Yudov
Module containing the formalization of normal modal logics. It includes: - Syntax and Kripke semantics of modal logics - Definition of modal logics K and S5 - Constructive proofs of...
## Description Sometimes the translation ends with an error: ```plaintext Uncaught (in promise) TypeError: Invalid type at yr (contentscript.js:2:313244) at contentscript.js:2:316449 ``` ## Configuration Sent to email [email protected] ## Environment...
### Version v23.3.0 ### Platform ```text Microsoft Windows NT 10.0.19045.0 x64 ``` ### Subsystem _No response_ ### What steps will reproduce the bug? 1. Install node.js on Windows in the...
# Steps to Reproduce ```idris import Data.So myVoid : (0 _ : Void) -> () myVoid x = void x foo : (y: Bool) -> (0 p : So y)...
# Description The following program prints `Error: Executed 'void'` when run. ```idris import Data.So myVoid : (0 _ : Void) -> () myVoid x = void x foo : (y:...
# Description Currently, the type constructor tag is always 100. In fact, they are not used. Therefore, I propose to remove them and also fix several related bugs. Commits: 1....
# Description Replaces `String` with `Name` in the `IBindVar` signature. This makes `IBindVar` more consistent and allows the binding of machine-generated names. Using machine-generated names in `IBindVar` can be useful...
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example...
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example...
# Steps to Reproduce In the following code, calling `f` with a double literal throws the error `Can't find an implementation for FromDouble Integer` ```idris f : Num a =>...