rzk-lang / rzk Goto Github PK
View Code? Open in Web Editor NEWAn experimental proof assistant based on a type theory for synthetic ∞-categories.
Home Page: https://rzk-lang.github.io/rzk/
An experimental proof assistant based on a type theory for synthetic ∞-categories.
Home Page: https://rzk-lang.github.io/rzk/
In the following formalisation, type parameters of flip
are not checked sufficiently:
#lang rzk-1
-- Flipping the arguments of a function.
#def flip
: (A : U) -> -- For any types A
(B : U) -> -- and B
(f : (x : A) -> (y : B) -> A) -> -- given a function f : A -> B -> A
((x : B) -> (y : A) -> A) -- we construct a function of type B -> A -> A
:= \A -> \B -> \f ->
\y -> \x -> f x y -- by swapping the arguments
-- Flipping a function twice is the same as not doing anything
#def flip-flip-is-id
: (A : 1) -> -- For any types A
(B : U) -> -- and B
(f : (x : A) -> (y : B) -> A) -> -- given a function f : A -> B -> A
flip A B (flip A B f) -- flip (flip f) <-- BUG HERE, should be flip B A (flip A B f)
=_{(x : A) -> (y : B) -> A} -- is identical
f -- to f
:= \A -> \B -> \f ->
refl_{f} -- proof by reflexivity
It would be nice to have syntax highlighting in VS Code.
It would be great to be able to import from files/URLs.
We have many syntax highlighting configs already:
minted
package for LaTeX. However, for best highlighting, these should be manually adjusted.Unfortunately, I'm not aware of a tool/approach that would allow to generate an acceptable version for all these in one go.
In any case, at least the HighlightJS is currently used in several repositories (e.g. this one, emilyriehl/yoneda, and fizruk/sHoTT). So at least that one should be factored out to be reused.
I can't tell whether the issue is with my computer or with the way I'm trying to typecheck in vscode or both. I can't find our previous discussion so I'm opening a new issue, but feel free to close and redirect me elsewhere.
My vscode extension is up to date.
From the terminal inside vscode I navigate into the hott folder of the yoneda repository and type rzk typecheck *-*.md
which yields the following error message:
rzk: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.33' not found (required by rzk)
rzk: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.34' not found (required by rzk)
rzk: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.32' not found (required by rzk)
But maybe this is the wrong way to go about it? When I navigate (still using the terminal inside vscode) over to the rzk repository I can typecheck successfully using stack exec rzk typecheck
followed by the path to the files.
In case it's relevant I'm running Ubuntu 20.04
There are two ways this should be possible:
trifecta
already is capable of producing regions for parsed parts of the AST, and can pretty print the context as textrzk
)Duplicate definitions at the top level should probably be considered an error.
There is a plugin for CodeMirror enabling Agda-input mode: https://github.com/Codewars/codemirror-agda
Type errors should hold information on the range (start and end positions) in the code where the type error occurred.
Currently, the generate_svgs.py
plugin is registered as a hook. To be able to reuse it with other projects that depend on rzk, it should be packaged as a proper MkDocs plugin and published on PyPI so that others can install and use it.
Possible configuration options:
Question: Is it desirable to automatically install rzk (from GitHub releases) if not found?
The following code makes the current typechecker go into an infinite loop:
#lang rzk-1
#def iscontr : (A : U) -> U
:= \A -> ∑ (a : A), (x : A) -> a =_{A} x
#def prod : (A : U) -> (B : U) -> U
:= \A -> \B -> ∑ (x : A), B
#def isweq : (A : U) -> (B : U) -> (f : (x : A) -> B) -> U
:= \A -> \B -> \f -> ∑ (g : (x : B) -> A), prod ((x : A) -> g (f x) =_{A} x) ((y : B) -> f (g y) =_{B} y)
#def weq : (A : U) -> (B : U) -> U
:= \A -> \B -> ∑ (f : (x : A) -> B), isweq A B f
#def relfunext : U
:=
(I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : (t : I) -> TOPE) ->
(A : <{t : I | psi t} -> U >) ->
(iscontrA : <{t : I | psi t} -> iscontr (A t) >) ->
(a : <{t : I | psi t /\ phi t} -> A t >) ->
<{t : I | psi t} -> A t [ psi t /\ phi t |-> a t]>
#def relfunext2 : U
:=
(I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : (t : I) -> TOPE) ->
(A : <{t : I | psi t} -> U >) ->
(a : <{t : I | psi t /\ phi t} -> A t >) ->
(f : <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>) ->
(g : <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>) ->
weq (f =_{<{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>} g)
<{t : I | psi t} -> f t =_{A t} g t [ psi t /\ phi t |-> refl_{f t} ]>
#def restrict
: (I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : (t : I) -> TOPE) ->
(A : (t : I) -> U) ->
(a : <{t : I | psi t} -> A t >) ->
<{t : I | psi t /\ phi t} -> A t >
:= \I -> \psi -> \phi -> \A -> \a ->
\t -> a t
#def ext-of-restrict
: (I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : (t : I) -> TOPE) ->
(A : (t : I) -> U) ->
(a : <{t : I | psi t} -> A t >) ->
<{t : I | psi t} -> A t [ psi t /\ psi t |-> restrict I psi phi A a t ]>
:= \I -> \psi -> \phi -> \A -> \a ->
\t -> a t
#def restricts-path
: (r : relfunext2) ->
(I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : (t : I) -> TOPE) ->
(A : (t : I) -> U) ->
(a_psi : <{t : I | psi t} -> A t >) ->
(a_phi : <{t : I | phi t} -> A t >) ->
(e : <{t : I | psi t /\ phi t} -> a_psi t =_{A t} a_phi t >) ->
restrict I psi phi A a_psi
=_{ <{t : I | psi t /\ phi t} -> A t > }
restrict I phi psi A a_phi
:=
\r ->
\I -> \psi -> \phi -> \A -> \a_psi -> \a_phi -> \e ->
(first (second (r I
(\t -> psi t /\ phi t)
(\t -> BOT)
(\t -> A t)
(\t -> recBOT)
(\t -> a_psi t)
(\t -> a_phi t)))) e
#def recOR-id
: (I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : (t : I) -> TOPE) ->
(A : (t : I) -> U) ->
(a_psi : <{t : I | psi t} -> A t >) ->
(a_phi : <{t : I | phi t} -> A t >) ->
(e : <{t : I | psi t /\ phi t} -> a_psi t =_{A t} a_phi t >) ->
<{t : I | psi t \/ phi t} -> A t >
:= \I -> \psi -> \phi -> \A -> \a_psi -> \a_phi -> \e ->
\t -> recOR(psi t, phi t, ext-of-restrict I psi phi A a_psi t, ext-of-restrict I phi psi A a_phi t)
The culprit is in the last line of the code. Note that it is not supposed to typecheck, but give a type error, since a_psi
and a_phi
are not definitionally equal on psi t /\ phi t
.
cabal install rzk
failed with the following error message:
Failed to build rzk-0.4.0.
Build log ( /Users/egbertrijke/.cabal/logs/ghc-9.4.4/rzk-0.4.0-3718e246.log ):
Configuring library for rzk-0.4.0..
Preprocessing library for rzk-0.4.0..
Building library for rzk-0.4.0..
[ 1 of 13] Compiling Free.Scoped ( src/Free/Scoped.hs, dist/build/Free/Scoped.o, dist/build/Free/Scoped.dyn_o )
[ 2 of 13] Compiling Free.Scoped.TH ( src/Free/Scoped/TH.hs, dist/build/Free/Scoped/TH.o, dist/build/Free/Scoped/TH.dyn_o )
[ 3 of 13] Compiling Language.Rzk.Syntax.Abs ( src/Language/Rzk/Syntax/Abs.hs, dist/build/Language/Rzk/Syntax/Abs.o, dist/build/Language/Rzk/Syntax/Abs.dyn_o )
[ 4 of 13] Compiling Language.Rzk.Syntax.Lex ( dist/build/Language/Rzk/Syntax/Lex.hs, dist/build/Language/Rzk/Syntax/Lex.o, dist/build/Language/Rzk/Syntax/Lex.dyn_o )
dist/build/Language/Rzk/Syntax/Lex.hs:572:50: error:
• Couldn't match expected type ‘Int16#’ with actual type ‘Int#’
• In the fifth argument of ‘alex_scan_tkn’, namely ‘sc’
In the expression:
alex_scan_tkn user__ input__ 0# input__ sc AlexNone
In the expression:
case alex_scan_tkn user__ input__ 0# input__ sc AlexNone of
(AlexNone, input__')
-> case alexGetByte input__ of
Nothing -> AlexEOF
Just _ -> AlexError input__'
(AlexLastSkip input__'' len, _) -> AlexSkip input__'' len
(AlexLastAcc k input__''' len, _)
-> AlexToken input__''' len (alex_actions ! k)
|
572 | = case alex_scan_tkn user__ input__ 0# input__ sc AlexNone of
| ^^
dist/build/Language/Rzk/Syntax/Lex.hs:602:1: error:
Couldn't match type ‘Int#’ with ‘Int16#’
Expected: t1
-> t2
-> Int#
-> AlexInput
-> Int16#
-> AlexLastAcc
-> (AlexLastAcc, (Posn, Char, [Byte], String))
Actual: t1
-> t2
-> Int#
-> (Posn, Char, [Byte], String)
-> Int#
-> AlexLastAcc
-> (AlexLastAcc, (Posn, Char, [Byte], String))
|
602 | alex_scan_tkn user__ orig_input len input__ s last_acc =
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
dist/build/Language/Rzk/Syntax/Lex.hs:617:27: error:
• Couldn't match expected type ‘Int#’ with actual type ‘Int32#’
• In the first argument of ‘(+#)’, namely ‘base’
In the expression: base +# ord_c
In an equation for ‘offset’: offset = (base +# ord_c)
|
617 | offset = (base +# ord_c)
| ^^^^
dist/build/Language/Rzk/Syntax/Lex.hs:620:73: error:
• Couldn't match expected type ‘Int#’ with actual type ‘Int16#’
• In the first argument of ‘(==#)’, namely ‘check’
In the first argument of ‘tagToEnum#’, namely ‘(check ==# ord_c)’
In the second argument of ‘(&&)’, namely
‘(tagToEnum# (check ==# ord_c))’
|
620 | new_s = if GTE(offset,0#) && EQ(check,ord_c)
| ^^^^^
dist/build/Language/Rzk/Syntax/Lex.hs:625:13: error:
• Couldn't match expected type ‘Int16#’ with actual type ‘Int#’
• In the pattern: -1#
In a case alternative: -1# -> (new_acc, input__)
In the expression:
case new_s of
-1# -> (new_acc, input__)
_ -> alex_scan_tkn
user__ orig_input
(if c < 0x80 || c >= 0xC0 then (len +# 1#) else len) new_input
new_s new_acc
|
625 | -1# -> (new_acc, input__)
| ^^^
[ 7 of 13] Compiling Language.Rzk.Syntax.Print ( src/Language/Rzk/Syntax/Print.hs, dist/build/Language/Rzk/Syntax/Print.o, dist/build/Language/Rzk/Syntax/Print.dyn_o )
src/Language/Rzk/Syntax/Print.hs:16:1: warning: [-Wunused-imports]
The import of ‘+, -’ from module ‘Prelude’ is redundant
|
16 | import Prelude (Bool (..), Double, Int, Integer,
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
src/Language/Rzk/Syntax/Print.hs:71:3: warning: [-Wunused-local-binds]
Defined but not used: ‘onNewLine’
|
71 | onNewLine i p = (if p then id else showChar '\n') . indent i
| ^^^^^^^^^
[10 of 13] Compiling Paths_rzk ( dist/build/autogen/Paths_rzk.hs, dist/build/Paths_rzk.o, dist/build/Paths_rzk.dyn_o )
[11 of 13] Compiling Rzk ( src/Rzk.hs, dist/build/Rzk.o, dist/build/Rzk.dyn_o )
Error: cabal: Failed to build rzk-0.4.0 (which is required by exe:rzk from
rzk-0.4.0). See the build log above for details.
It is inconvenient to have to copy-paste expressions or introduce auxiliary definitions to imitate let
-bindings. And this is a simple extension, so can be added in the current prototype.
I guess we need #fail
command in Rzk to mark definitions that should fail (and check that it fails indeed).
Originally posted by @fizruk in emilyriehl/yoneda#39 (comment)
At the moment rzk-1
prototype does not handle currying of extension functions [RS17, Theorem 4.2] correctly. Consider the following snippet:
The output hints that it cannot identify k (t, s) = f (t, s)
since zeta s
constraint is not available for some reason (it should be):
Local tope context:
phi t
psi t
Expected type
f
but inferred
k
when trying to unify expected type
λs → f ((t, s))
with inferred type
λs → k ((t, s))
for the term
λt → λs → k ((t, s))
With rzk v0.5, when trying to typecheck yoneda/src/simplicial-hott/04-extension-types.rzk.md, I'm getting:
src/simplicial-hott/04-extension-types.rzk.md:
Error occurred when checking
#define flip-ext-fun
undefined variable: Eq
I get the same error when permuting the definitions, e.g. putting curry-uncurry before.
To reduce boilerplate in formalisations, it makes sense to introduce some simple organisational features, such as sections and variables (shared assumptions). I've implemented a version of these in develop
, getting inspired by Lean and Coq. I ended up with Coq-style variables, but I'm not sure which one is better and why. Below are some examples and some of my thoughts.
Lean4 has Variables which can be used to automatically add bound variables to the following definitions:
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)
def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
def plus4 := compose _ _ _ (fun x => x + 2) (fun x => x + 2)
Important properties of variable
declaration in Lean4:
compose
will not have h
as its bound variable, but will have α
, β
, γ
, g
, f
, and x
bound variables. On the other hand, doTwice
and doThrice
only depend on α
, h
, and x
.variable {α β γ : Type}
), even inside the same section. This is why plus4
calls compose
with all 5 arguments.Coq has Assumptions, including Variable
and Hypothesis
commands (which are equivalent).
Section example.
Variable (α β γ : Type).
Section compose.
Variable (g : β → γ) (f : α → β) (h : α → α).
Variable (x : α).
Define compose := g (f x).
Define doTwice := h (h x).
Define doThrice := h (h (h x)).
(* Define plus4 := compose. PROBLEM: compose is already saturated (fully applied). *)
End compose.
(* Type variables are already in scope. *)
(* But g, f, and x become explicit arguments. *)
Def plus4 := compose (fun x => x + 2) (fun x => x + 2).
End example.
(* Outside of section "example", type variables become explicit arguments. *)
Def plus4' := compose _ _ _ (fun x => x + 2) (fun x => x + 2).
Important properties of Variable
command in Coq:
Similarly to Lean, only variables that are actually used in a definition are introduced as parameter upon exiting a section.
In contrast to Lean, variables are implicit in applications of definitions in the same section (this means that sometimes you need to exit section before you can properly use it).
There is an implementation of Coq-style variables and sections (see 469cde5, or develop
branch at the time of writing). You can see an example use of this here: https://github.com/fizruk/rzk/blob/37708d49aa50fe866a4c54370b827b9ff0c6b1ca/docs/docs/rzk-1/recId.md?plain=1#L80-L187.
Originally, this seemed to be a nice approach, however, I now think this is setting up an issue:
it is too easy to accidentally use an extra assumption. For example, it is tempting to set #variable AisSegal : isSegal A
to make the proof assistant automatically figure out when it is used, even when it is implicit. In particular, it would make it easy to use conclusion as assumption (e.g. when proving that A is Segal using a lemma that indirectly uses AisSegal
).
This is less of a problem if we use Lean-style variables, since we would have to write AisSegal
explicitly in the proof and will probably notice it. However, this might still become a problem once we add term inference and write _
instead of AisSegal
(or a similar argument), or when it is introduced indirectly somehow (I would have to think of an example).
This suggests to me two things:
There is a strong need in a language server (see #31) to make sure users have easy access to see explicitly all assumptions of a definition.
It might make sense to add some extra checks/warnings when an assumption matches (exactly?) the conclusion in a definition.
Syntax introduced in rzk-0.2.0
is not documented properly yet.
It would be great to be able to work with shapes as types.
There is currently no syntax for shape inclusion, which is sometimes an inconvenience. For example, formulating relative function extensionality like this does not work:
#def relfunext : U
:=
(I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : {(t : I) | psi t} -> TOPE) ->
(A : <{t : I | psi t} -> U >) ->
(iscontrA : <{t : I | psi t} -> iscontr (A t) >) ->
(a : <{t : I | phi t} -> A t >) ->
<{t : I | psi t} -> A t [ phi t |-> a t]>
Currently this causes a type error when typechecking a
:
Cannot satisfy the tope constraint:
psi t
in local tope context
when typechecking term
phi t
Temporary solution is to rely on intersection of shapes to imply inclusion:
#def relfunext : U
:=
(I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : (t : I) -> TOPE) ->
(A : <{t : I | psi t} -> U >) ->
(iscontrA : <{t : I | psi t} -> iscontr (A t) >) ->
(a : <{t : I | psi t /\ phi t} -> A t >) ->
<{t : I | psi t} -> A t [ psi t /\ phi t |-> a t]>
Apparently, this happens because GHCJS linker is running out of memory.
It is unclear what exactly causes this and how to properly fix it.
Perhaps, it might make sense to make a put the latest built JS binaries in a separate directory on gh-pages
, and then remove all the experimental code for STLC, PCF, and MLTT, leaving only pure rzk-1
supported in new releases. This should significantly reduce the size of Haskell sources, so probably should help with the memory usage in GHCJS.
#def bug (A : U) (x : A) (y : A) (z : A) : U
:= {(t, s) : 2 * 2} -> A [ t === 0_2 |-> x, t === s |-> z]
Restriction types with multiple restrictions should have a coherence check, which appears to be missing.
The Rzk.TypeCheck
module is now over 3k LoC and includes a lot of extra code. Should split into multiple modules and properly document.
E.g. via optparse-generic.
Similar to #define
, but would only introduce local definitions, unavailable from outside a section. Similar to Let
command in Coq.
Seems to be non-trivial, but doable. Would help to just be able to install binaries without having to build everything from sources.
Hi! This is a small feature request for the ability to write rzk --version
or rzk -v
in the terminal to figure out which version is used. This would benefit me as I'm easily confused by the Haskell package management tools. :)
I assume this is a sub-issue of #30, but I figured I could post the request regardless.
Currently, all axioms have to be dragged explicitly as function dependencies.
However, it is not difficult to postulate axioms.
Some useful axioms are the relative function extensionality and monotonicity of 𝟚 → 𝟚
.
The following snippet fails to typecheck, because global x
conflicts with local x
in the definition of hom
, for some reason.
#lang rzk-1
-- 1-simplex
#def Δ¹ : (t : 2) -> TOPE
:= \(t : 2) -> TOP
-- boundary of a 1-simplex
#def ∂Δ¹ : (t : 2) -> TOPE
:= \(t : 2) -> (t === 0_2 \/ t === 1_2)
-- boundary of a 2-simplex
#def ∂Δ² : (t : 2 * 2) -> TOPE
:= \(t, s) -> (s === 0_2 \/ t === 1_2 \/ s === t)
-- 2-simplex
#def Δ² : (t : 2 * 2) -> TOPE
:= \(t, s) -> s <= t
-- the (2,1)-horn
#def Λ : (t : 2 * 2) -> TOPE
:= \(t, s) -> (s === 0_2 \/ t === 1_2)
-- [RS17, Definition 5.1]
-- The type of arrow in A from x to y
#def hom : (A : U) -> (x : A) -> (y : A) -> U
:= \A -> \x -> \y -> <{t : 2 | Δ¹ t } -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ]>
#def x : U
:= U
It seems that the rzk
type checker does not know how to handle code blocks with attributes in markdown.
For instance, the following code is completely ignored:
```rzk title="Rijke 22, Definition 9.3.1"
#def Eq-Σ
( s t : Σ (a : A) , B a)
: U
:=
Σ ( p : (first s) = (first t)) ,
( transport A B (first s) (first t) p (second s)) = (second t)
```
The same happens if the attributes are wrapped in curly braces.
When I have two code blocks with attributes back to back, however, I get the following error:
An error occurred when parsing file src/hott/05-sigma.rzk.md
rzk: syntax error at end of file
CallStack (from HasCallStack):
error, called at src/Rzk/Main.hs:67:9 in rzk-0.5.1-fd1942b5:Rzk.Main
The idea is to typecheck an expression (or infer its type) without giving it a name. Can be useful, e.g. to check that components of equivalences compute to desired mappings.
In particular, it seems that build-tools
have to be specified. #43 might be related.
We are currently using CodeMirror 5 which is not supported anymore, as far as I can see.
Consider the following snippet:
The last definition here does not typecheck, as hom A x y
is failing to unify with (essentially) itself:
Local tope context:
(t ≡ 0) ∨ (t ≡ 1)
⊤
Expected type
rec∨(t ≡ 0, t ≡ 1, x, y)
but inferred
x
when trying to unify expected type
〈{t : 𝟚 | ⊤} → A[ ((t ≡ 0) ∨ (t ≡ 1)) ↦ rec∨(t ≡ 0, t ≡ 1, x, y) ]〉
with inferred type
((hom A) x) y
for the term
f
Failed to typecheck due to a type error!
A command to compute a term (to WHNF or NF). Can be useful for debugging.
Rzk already has partial support in LaTeX (with the minted
package, see here). Would be nice to also typecheck these files.
The following code is incomplete:
This might not be critical, as it only affects used
implicit variables checks, which work in a way that should collect all transitive dependencies anyway. But it would be great to fix this and, moreover, to be able to cache/reuse the set of free variables efficiently.
Currently, we do not have coproducts, as they are not used in RS17. But it would be nice to have them.
At least, we should support Markdown files with rzk
blocks and check that examples in the documentation work on CI.
It seems that some conveniences strongly require implicit arguments, so it would be good to get those soon.
Minimal example:
#lang rzk-1
#section left-open
Resulting error
> rzk typecheck test.rzk
Loading file /src/test.rzk
An error occurred when parsing file /src/test.rzk
rzk: syntax error at end of file
CallStack (from HasCallStack):
error, called at src/Rzk/Main.hs:79:11 in rzk-0.5.6-77841b86eb45b408582f63a681be46bfa60dae786116e8a3336e01207426afe9:Rzk.Main
A more informative error expliciting that a section has been left open (and its name) would be great.
Trying to render a tetrahedron carved from a prism:
#set-option "render" = "svg"
-- The Segal-associativity-witness curries to define a diagram Δ²×Δ¹ -> A.
-- The Segal-associativity-tetrahedron is extracted via the middle-simplex map \((t, s), r) -> ((t, r), s) from Δ³ to Δ²×Δ¹
#def Segal-associativity-tetrahedron
(extext : ExtExt) -- This proof uses extension extensionality.
(A : U) -- A type.
(AisSegal : isSegal A) -- A proof that A is Segal.
(w x y z : A) -- Four points in A.
(f : hom A w x) -- An arrow in A from w to x.
(g : hom A x y) -- An arrow in A from x to y.
(h : hom A y z) -- An arrow in A from y to z.
: Δ³ -> A
:= \((t, s), r) ->
(\{(t1, (t2, t3)) : 2 * (2 * 2) | t2 <= t1 } ->(Segal-associativity-witness extext A AisSegal w x y z f g h) (t1, t2) t3) (t, (r, s))
#set-option "render" = "none"
Yields empty SVG.
For better integration with IDEs.
Name shadowing should produce a warning (if not an error).
I really like Lean's Auto Bound Implicit Arguments and I think they should not be difficult to implement, at least once unification is added to rzk.
The following code does not work:
#lang rzk-1
#def prod : (A : U) -> (B : U) -> U
:= \A -> \B -> ∑ (x : A), B
#def isweq : (A : U) -> (B : U) -> (f : (x : A) -> B) -> U
:= \A -> \B -> \f -> ∑ (g : (x : B) -> A), prod ((x : A) -> g (f x) =_{A} x) ((y : B) -> f (g y) =_{B} y)
#def weq : (A : U) -> (B : U) -> U
:= \A -> \B -> ∑ (f : (x : A) -> B), isweq A B f
#def relfunext2 : U
:=
(I : CUBE) ->
(psi : (t : I) -> TOPE) ->
(phi : (t : I) -> TOPE) ->
(A : <{t : I | psi t} -> U >) ->
(a : <{t : I | psi t /\ phi t} -> A t >) ->
(f : <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>) ->
(g : <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>) ->
weq (f =_{<{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>} g)
<{t : I | psi t} -> f t =_{A t} g t [ psi t /\ phi t |-> refl_{f t} ]>
#def bug : (r : relfunext2) -> relfunext2
:= \r -> r
It seems that there is still a problem with handling of bound variables, so expansion of relfunext2
type is done incorrectly.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.