brew install ssreflect
git clone https://github.com/mathink/Cat_on_Coq
cd Cat_on_Coq
perl -i -pe 's/COC\.//g' *.v
perl -i -pe 's/-R \. COC//' _CoqProject
make all
emacs Functor.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
main.cpp: メンバ関数 ‘void yakkai::interpreter::gc::mark_stack()’ 内: | |
main.cpp:1479:26: エラー: expected primary-expression before ‘void’ | |
main.cpp:1479:32: エラー: ‘alignas’ was not declared in this scope | |
main.cpp:1479:34: エラー: expected ‘;’ before ‘int’ | |
main.cpp:1482:63: エラー: ‘_dummy_stack_end_object’ was not declared in this scope | |
main.cpp:1482:87: エラー: unable to deduce ‘auto’ from ‘<expression error>’ | |
main.cpp:1488:65: エラー: unable to deduce ‘auto’ from ‘<expression error>’ | |
main.cpp: メンバ関数 ‘yakkai::node* yakkai::interpreter::machine::call_function(const yakkai::node*, yakkai::cons*, const std::shared_ptr<yakkai::interpreter::scope>&, const std::shared_ptr<yakkai::interpreter::scope>&)’ 内: | |
main.cpp:1678:26: 警告: 使用されない変数 ‘reached_to_last_parameter’ です [-Wunused-variable] | |
main.cpp: メンバ関数 ‘yakkai::node* yakkai::interpreter::machine::add(yakkai::cons*, const std::shared_ptr<yakkai::interpreter::scope>&)’ 内: |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(assume JSON) | |
(assume newVue) | |
(assume newXMLHttpRequest) | |
(newVue (object | |
el "#demo" | |
data (object branch "master") | |
created (^ () (seq | |
(assume this) | |
((. this $watch) "branch" (^ () ((. this fetchData)))))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import List. | |
Require Import Coq.Bool.Bool. | |
Require Import Coq.Arith.EqNat. | |
Require Import Coq.Lists.ListSet. | |
Definition nat_eq : forall x y : nat, {x = y} + {x <> y}. | |
decide equality. | |
Defined. | |
Inductive term : Set := |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
console : log of (simple string -> simple unit) | |
& info of (simple string -> simple unit); | |
console.log "hello world" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Token ","; | |
Token ";"; | |
Syntax "$a ; $b" := "@SEQUENCE $a $b", | |
level 1, right associativity; | |
Syntax "Token $a" := "@TOKEN $a", | |
level 2, no associativity; | |
Syntax "Syntax $a := $b, level $c, $d associativity" := "@SYNTAX $a $b $c $d", |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
function isMetaVariable(tk) { | |
return tk[0] === '$'; | |
} | |
function subst(env, replacement) { | |
if (Array.isArray(replacement)) { | |
return replacement.map(function (item) { return subst(env, item); }); | |
} else if (isMetaVariable(replacement)) { | |
return env[replacement]; | |
} else { |
procedural.lthstx というファイルで構文を定義しています。 まだ処理系は公開していませんが、現在これが期待した通りに動作するよう実装できています。
構文は完全に宣言的に定義されているので、それ自体が構文仕様になります。