try it out: https://marklemay.github.io/ddynamic-web/
a minimal dependently typed langugage where deffintional equality can be resolved dynamically at runtime.
The project is tested in the following environment(s):
- GHC 9.6.1 and cabal 3.10.1.0
To load the surface repl
cabal new-run repl
supports commands for
- loadfiles, cast elaboration
:l - quit
:q - check type of an expression
:t - normalize expression
:n - enter an expression without a prefix attempts to get all information from it, typing/normalization/..
for example
dt-surface> :l ex/a0.dt
parsed
elaborated
cleaned
loaded
dt> :t not
not : Bool -> Bool
dt> :n not true
not true
: Bool
~>
false
dt> not (not (true))
not (not true)
: Bool
~>
true
To run the haskell project: cabal new-repl
To run the test suit: cabal new-test