name: Security audit | |
on: | |
schedule: | |
- cron: '0 0 * * *' | |
push: | |
paths: | |
- '**/Cargo.toml' | |
- '**/Cargo.lock' | |
jobs: | |
security_audit: |
;; Copyright 2020 Nicolas Rougier - BSD License | |
;; Usage: emacs -q -l bordered.el | |
(set-face-font 'default "Roboto Mono Light 14") | |
(setq default-frame-alist | |
(append (list '(width . 72) '(height . 40) | |
'(vertical-scroll-bars . nil) | |
'(internal-border-width . 0) | |
'(font . "Roboto Mono Light 14")))) | |
(set-frame-parameter (selected-frame) | |
'internal-border-width 0) |
I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.
Q: What is cubical type theory?
A: It’s a type theory giving homotopy type theory its computational meaning.
Q: What is homotopy type theory then?
A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.
-- Note: There is a more complete explanation at https://github.com/hwayne/lets-prove-leftpad/tree/master/idris | |
import Data.Vect | |
-- `minus` is saturating subtraction, so this works like we want it to | |
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k | |
eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl | |
eq_max Z (S _) = Refl | |
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl | |
-- The type here says "the result is" padded to (maximum k n), and is padding plus the original |
a4b.amazonaws.com | |
access-analyzer.amazonaws.com | |
account.amazonaws.com | |
acm-pca.amazonaws.com | |
acm.amazonaws.com | |
airflow-env.amazonaws.com | |
airflow.amazonaws.com | |
alexa-appkit.amazon.com | |
alexa-connectedhome.amazon.com | |
amazonmq.amazonaws.com |
WARNING
This gist is outdated! For the most up-to-date information, please see http://emberjs.com/guides/routing/!
An Ember application starts with its main template. Put your header, footer, and any other decorative content in application.handlebars
.
<header>
package wolv.parserlibproblem | |
import util.parsing.ast.AbstractSyntax | |
import util.parsing.combinator.syntactical.TokenParsers | |
import util.parsing.combinator.lexical.Lexical | |
import util.parsing.combinator.token.Tokens | |
trait SimpleTokens extends Tokens { | |
case class Foo extends Token | |
case class Bar extends Token |